Mathbox for Scott Fenton 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > dfoutsideof  Unicode version 
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, 17Oct2013.) 
Ref  Expression 

dfoutsideof  OutsideOf 
Step  Hyp  Ref  Expression 

1  coutsideof 25767  . 2 OutsideOf  
2  ccolin 25685  . . 3  
3  cbtwn 25542  . . 3  
4  2, 3  cdif 3260  . 2 
5  1, 4  wceq 1649  1 OutsideOf 
Colors of variables: wff set class 
This definition is referenced by: broutsideof 25769 
Copyright terms: Public domain  W3C validator 