Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-outsideof Structured version   Visualization version   GIF version

Definition df-outsideof 31866
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
StepHypRef Expression
1 coutsideof 31865 . 2 class OutsideOf
2 ccolin 31783 . . 3 class Colinear
3 cbtwn 25669 . . 3 class Btwn
42, 3cdif 3552 . 2 class ( Colinear ∖ Btwn )
51, 4wceq 1480 1 wff OutsideOf = ( Colinear ∖ Btwn )
Colors of variables: wff setvar class
This definition is referenced by:  broutsideof  31867
  Copyright terms: Public domain W3C validator