Theorem broutsideof

Description: Binary relation form of OutsideOf . Theorem 6.4 of Schwabhauser p. 43. (Contributed by Scott Fenton, 17-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	broutsideof	|- ( P OutsideOf <. A , B >. <-> ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) )

Proof

Step	Hyp	Ref	Expression
1		df-outsideof	|- OutsideOf = ( Colinear \ Btwn )
2	1	breqi	|- ( P OutsideOf <. A , B >. <-> P ( Colinear \ Btwn ) <. A , B >. )
3		brdif	|- ( P ( Colinear \ Btwn ) <. A , B >. <-> ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) )
4	2 3	bitri	|- ( P OutsideOf <. A , B >. <-> ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) )