:: deftheorem defines cong GTARSKI1:def 3 :
for S being TarskiGeometryStruct
for a, b, c, x, y, z being POINT of S holds
( a,b,c cong x,y,z iff ( a,b equiv x,y & a,c equiv x,z & b,c equiv y,z ) );