Definition df-outsideof

Description: The outside of relationship. This relationship expresses that P , A , and B fall on a line, but P is not on the segment A B . 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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coutsideof	⊢ OutsideOf
1		ccolin	⊢ Colinear
2		cbtwn	⊢ Btwn
3	1 2	cdif	⊢ ( Colinear ∖ Btwn )
4	0 3	wceq	⊢ OutsideOf = ( Colinear ∖ Btwn )