Definition df-outsideof 34422

Description: The outside of relationship. This relationship expresses that 𝑃, 𝐴, and 𝐵 fall on a line, but 𝑃 is not on the segment 𝐴𝐵. This definition is taken from theorem 6.4 of [Schwabhauser] p. 43, since it requires no dummy variables. (Contributed by Scott Fenton, 17-Oct-2013.)

Assertion

Ref	Expression
df-outsideof	⊢ OutsideOf = ( Colinear ∖ Btwn )

Detailed syntax breakdown of Definition df-outsideof

Step	Hyp	Ref	Expression
1		coutsideof 34421	. 2 class OutsideOf
2		ccolin 34339	. . 3 class Colinear
3		cbtwn 27257	. . 3 class Btwn
4	2, 3	cdif 3884	. 2 class ( Colinear ∖ Btwn )
5	1, 4	wceq 1539	1 wff OutsideOf = ( Colinear ∖ Btwn )

This definition is referenced by:  broutsideof  34423