let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for b, c, p being POINT of S holds Middle reflection (p,c), reflection (p,b), reflection (p,(reflection (b,c)))
let b, c, p be POINT of S; :: thesis: Middle reflection (p,c), reflection (p,b), reflection (p,(reflection (b,c)))
Middle c,b, reflection (b,c) by GTARSKI3:def 13;
then ( between reflection (p,c), reflection (p,b), reflection (p,(reflection (b,c))) & reflection (p,b), reflection (p,c) equiv reflection (p,b), reflection (p,(reflection (b,c))) ) by GTARSKI3:def 12, GTARSKI3:106, GTARSKI3:107;
hence Middle reflection (p,c), reflection (p,b), reflection (p,(reflection (b,c))) by GTARSKI3:def 12; :: thesis: verum