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

Definition df-outsideof 24153
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
StepHypRef Expression
1 coutsideof 24152 . 2  class OutsideOf
2 ccolin 24070 . . 3  class  Colinear
3 cbtwn 23927 . . 3  class  Btwn
42, 3cdif 3150 . 2  class  (  Colinear  \  Btwn  )
51, 4wceq 1623 1  wff OutsideOf  =  ( 
Colinear  \  Btwn  )
Colors of variables: wff set class
This definition is referenced by:  broutsideof  24154
  Copyright terms: Public domain W3C validator