let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, x, a9, b9, c9, x9 being POINT of S st a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 holds
c,x equiv c9,x9
let a, b, c, x, a9, b9, c9, x9 be POINT of S; :: thesis: ( a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 implies c,x equiv c9,x9 )
S is satisfying_SAS ;
hence ( a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 implies c,x equiv c9,x9 ) ; :: thesis: verum