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 31397
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 31396 . 2 class OutsideOf
2 ccolin 31314 . . 3 class Colinear
3 cbtwn 25569 . . 3 class Btwn
42, 3cdif 3537 . 2 class ( Colinear ∖ Btwn )
51, 4wceq 1475 1 wff OutsideOf = ( Colinear ∖ Btwn )
Colors of variables: wff setvar class
This definition is referenced by:  broutsideof  31398
  Copyright terms: Public domain W3C validator