:: deftheorem defines (Eu) GTARSKI3:def 24 :
for S being TarskiGeometryStruct holds
( S is (Eu) iff for a, b, c, d, t being POINT of S st between a,d,t & between b,d,c & a <> d holds
ex x, y being POINT of S st
( between a,b,x & between a,c,y & between x,t,y ) );