:: deftheorem defines satisfying_SAS GTARSKI1:def 9 :
for S being TarskiGeometryStruct holds
( S is satisfying_SAS iff for a, b, c, x, a1, b1, c1, x1 being POINT of S st a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 holds
c,x equiv c1,x1 );