Nuprl Definition : geo-tar-same-side
geo-tar-same-side(e;a;b;p;q) ==  ∃c:Point. (geo-tar-opp-side(e;a;c;p;q) ∧ geo-tar-opp-side(e;b;c;p;q))
Definitions occuring in Statement : 
geo-tar-opp-side: geo-tar-opp-side(e;a;b;p;q)
, 
geo-point: Point
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
Definitions occuring in definition : 
exists: ∃x:A. B[x]
, 
geo-point: Point
, 
and: P ∧ Q
, 
geo-tar-opp-side: geo-tar-opp-side(e;a;b;p;q)
FDL editor aliases : 
geo-tar-same-side
geo-tar-same-side
Latex:
geo-tar-same-side(e;a;b;p;q)  ==
    \mexists{}c:Point.  (geo-tar-opp-side(e;a;c;p;q)  \mwedge{}  geo-tar-opp-side(e;b;c;p;q))
Date html generated:
2017_10_02-PM-06_23_14
Last ObjectModification:
2017_08_05-PM-04_17_26
Theory : euclidean!plane!geometry
Home
Index