for a, b, c, a1, b1, c1 being POINT of TarskiEuclid2Space holds
( a,b,c cong a1,b1,c1 iff ( dist (a,b) = dist (a1,b1) & dist (a,c) = dist (a1,c1) & dist (b,c) = dist (b1,c1) ) ) by GTARSKI1:def 15;