let X, Y be Subset of TarskiEuclid2Space; :: thesis: 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 ) & a in Y & not X = {a} holds
X is empty
let a be Element of TarskiEuclid2Space; :: thesis: ( ( for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y ) & a in Y & not X = {a} implies X is empty )
assume that
A1: for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y and
A2: a in Y ; :: thesis: ( X = {a} or X is empty )
M1: X c= {a}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {a} )
assume L1: x in X ; :: thesis: x in {a}
then reconsider x = x as Element of TarskiEuclid2Space ;
a = x by GTARSKI1:def 10, A1, A2, L1;
hence x in {a} by TARSKI:def 1; :: thesis: verum

end;

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: ( X = {a} or X is empty )

hence ( X = {a} or X is empty ) ; :: thesis: verum

end;

suppose not X is empty ; :: thesis: ( X = {a} or X is empty )

then consider x being object such that
A3: x in X ;
reconsider x = x as Element of TarskiEuclid2Space by A3;
a = x by GTARSKI1:def 10, A1, A2, A3;
then {a} c= X by TARSKI:def 1, A3;
hence ( X = {a} or X is empty ) by M1; :: thesis: verum

end;

end;