let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, p being POINT of S
for A being Subset of S st A is_line & a in A & p in A holds
reflection (p,a) in A
let a, p be POINT of S; :: thesis: for A being Subset of S st A is_line & a in A & p in A holds
reflection (p,a) in A
let A be Subset of S; :: thesis: ( A is_line & a in A & p in A implies reflection (p,a) in A )
assume that
A1: A is_line and
A2: a in A and
A3: p in A ; :: thesis: reflection (p,a) in A

per cases ( p = a or p <> a ) ;

suppose p = a ; :: thesis: reflection (p,a) in A

hence reflection (p,a) in A by A2, GTARSKI3:104; :: thesis: verum

end;

suppose A4: p <> a ; :: thesis: reflection (p,a) in A

Middle a,p, reflection (p,a) by GTARSKI3:def 13;
then Collinear p,a, reflection (p,a) by GTARSKI4:7;
then reflection (p,a) in Line (p,a) ;
hence reflection (p,a) in A by A4, A1, A2, A3, GTARSKI3:87; :: thesis: verum

end;

end;