let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, p being POINT of S st a <> p holds
reflection (a,p) <> p
let a, b, p be POINT of S; :: thesis: ( a <> p implies reflection (a,p) <> p )
assume A1: a <> p ; :: thesis: reflection (a,p) <> p
assume A2: p = reflection (a,p) ; :: thesis: contradiction
Middle p,a, reflection (a,p) by GTARSKI3:def 13;
hence contradiction by GTARSKI3:97, A1, A2; :: thesis: verum