for a, b being POINT of TarskiEuclid2Space holds a,b equiv b,a

proof

let a, b be POINT of TarskiEuclid2Space; :: thesis: a,b equiv b,a
dist (a,b) = dist (b,a) ;
hence a,b equiv b,a by GTARSKI1:def 15; :: thesis: verum

end;

hence TarskiEuclid2Space is satisfying_CongruenceSymmetry ; :: thesis: verum