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	$$⊢\mathrm{OutsideOf}=\mathrm{Colinear}\setminus \mathrm{Btwn}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coutsideof	$$class\mathrm{OutsideOf}$$
1		ccolin	$$class\mathrm{Colinear}$$
2		cbtwn	$$class\mathrm{Btwn}$$
3	1 2	cdif	$$class\left(\mathrm{Colinear}\setminus \mathrm{Btwn}\right)$$
4	0 3	wceq	$$wff\mathrm{OutsideOf}=\mathrm{Colinear}\setminus \mathrm{Btwn}$$