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

proof

Middle a,p, reflection (p,a) by GTARSKI3:def 13;
hence between a,p, reflection (p,a) ; :: thesis: verum

end;

A6: reflection (p,a) <> p

proof

assume reflection (p,a) = p ; :: thesis: contradiction
then Middle a,p,p by GTARSKI3:def 13;
hence contradiction by A2, A4, GTARSKI1:def 7; :: thesis: verum

end;

A7: between b,p, reflection (p,a) by A5, A3, A6, GTARSKI3:71;
N1: not b in A

proof

assume b in A ; :: thesis: contradiction
then A8: Line (p,b) = A by A3, A1, A2, GTARSKI3:87;
Collinear a,p,b by A3, GTARSKI3:73;
then Collinear p,b,a ;
hence contradiction by A8, A4; :: thesis: verum

end;

not reflection (p,a) in A

proof

assume reflection (p,a) in A ; :: thesis: contradiction
then A9: Line (p,(reflection (p,a))) = A by A2, A1, A6, GTARSKI3:87;
Collinear p, reflection (p,a),a by A5;
hence contradiction by A9, A4; :: thesis: verum

end;

hence between b,A, reflection (p,a) by N1, A1, A2, A7; :: thesis: verum