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 )