MetrStruct(# the U1 of TarskiEuclid2Space, the distance of TarskiEuclid2Space #) = MetrStruct(# the U1 of (Euclid 2), the distance of (Euclid 2) #) by GTARSKI1:def 13;
then reconsider a = |[0,0]|, b = |[1,0]|, c = |[0,1]| as Point of TarskiEuclid2Space by EUCLID:22;
take a ; :: thesis: ex b, c being Point of TarskiEuclid2Space st
( not between a,b,c & not between b,c,a & not between c,a,b )
take b ; :: thesis: ex c being Point of TarskiEuclid2Space st
( not between a,b,c & not between b,c,a & not between c,a,b )
take c ; :: thesis: ( not between a,b,c & not between b,c,a & not between c,a,b )
thus not between a,b,c :: thesis: ( not between b,c,a & not between c,a,b )
proof
assume between a,b,c ; :: thesis: contradiction
then Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c)) by ThConv6;
then (dist ((Tn2TR a),(Tn2TR b))) + (dist ((Tn2TR b),(Tn2TR c))) = dist ((Tn2TR a),(Tn2TR c)) by EUCLID12:12;
hence contradiction by SQUARE_1:19, THY1, THY2, THY3; :: thesis: verum
end;
thus not between b,c,a :: thesis: not between c,a,b
proof
assume between b,c,a ; :: thesis: contradiction
then Tn2TR c in LSeg ((Tn2TR b),(Tn2TR a)) by ThConv6;
then (dist ((Tn2TR b),(Tn2TR c))) + (dist ((Tn2TR c),(Tn2TR a))) = dist ((Tn2TR b),(Tn2TR a)) by EUCLID12:12;
hence contradiction by SQUARE_1:19, THY1, THY2, THY3; :: thesis: verum
end;
assume between c,a,b ; :: thesis: contradiction
then Tn2TR a in LSeg ((Tn2TR c),(Tn2TR b)) by ThConv6;
then (dist ((Tn2TR c),(Tn2TR a))) + (dist ((Tn2TR a),(Tn2TR b))) = dist ((Tn2TR c),(Tn2TR b)) by EUCLID12:12;
hence contradiction by SQUARE_1:21, THY1, THY2, THY3; :: thesis: verum