let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, p, q, r, s being POINT of S holds
( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) )
let a, p, q, r, s be POINT of S; :: thesis: ( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) )

now :: thesis: ( reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) implies ( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) ) )

assume reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) ; :: thesis: ( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) )
( reflection (a,(reflection (a,p))) = p & reflection (a,(reflection (a,q))) = q & reflection (a,(reflection (a,r))) = r & reflection (a,(reflection (a,s))) = s ) by Satz7p7;
hence ( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) ) by Lemma7p16a; :: thesis: verum

end;

hence ( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) ) by Lemma7p16a; :: thesis: verum