for a, b, c, d, t being Element of TarskiEuclid2Space st between a,d,t & between b,d,c & a <> d holds
ex x, y being Element of TarskiEuclid2Space st
( between a,b,x & between a,c,y & between x,t,y )