Definition df-outsideof 33576

Description: The outside of relationship. This relationship expresses that 𝑃, 𝐴, and 𝐵 fall on a line, but 𝑃 is not on the segment 𝐴𝐵. 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 33575	. 2 class OutsideOf
2		ccolin 33493	. . 3 class Colinear
3		cbtwn 26669	. . 3 class Btwn
4	2, 3	cdif 3932	. 2 class ( Colinear ∖ Btwn )
5	1, 4	wceq 1533	1 wff OutsideOf = ( Colinear ∖ Btwn )

This definition is referenced by:  broutsideof  33577