Definition df-outsideof 32227

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.)

Assertion

Ref	Expression
df-outsideof	|- OutsideOf = ( Colinear \ Btwn )

Detailed syntax breakdown of Definition df-outsideof

Step	Hyp	Ref	Expression
1		coutsideof 32226	. 2 class OutsideOf
2		ccolin 32144	. . 3 class Colinear
3		cbtwn 25769	. . 3 class Btwn
4	2, 3	cdif 3571	. 2 class ( Colinear \ Btwn )
5	1, 4	wceq 1483	1 wff OutsideOf = ( Colinear \ Btwn )

This definition is referenced by:  broutsideof  32228