theorem :: GTARSKI2:50

for X, Y being Subset of TarskiEuclid2Space
for a being Element of TarskiEuclid2Space st ( for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y ) & not X is empty & not Y is empty & ( X is trivial implies X <> {a} ) holds
ex b being Element of TarskiEuclid2Space st
( X c= Line ((Tn2TR a),(Tn2TR b)) & Y c= Line ((Tn2TR a),(Tn2TR b)) )