let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a being POINT of S
for A being Subset of S st A is_line & not a in A holds
ex c being POINT of S st between a,A,c
let a be POINT of S; :: thesis: for A being Subset of S st A is_line & not a in A holds
ex c being POINT of S st between a,A,c
let A be Subset of S; :: thesis: ( A is_line & not a in A implies ex c being POINT of S st between a,A,c )
assume that
A1: A is_line and
A2: not a in A ; :: thesis: ex c being POINT of S st between a,A,c
consider p, q being POINT of S such that
A3: p <> q and
A4: A = Line (p,q) by A1;
A5: ( p in A & q in A ) by A4, GTARSKI3:83;
set c = reflection (p,a);
A6: p <> reflection (p,a)

proof

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

end;

take reflection (p,a) ; :: thesis: between a,A, reflection (p,a)
A7: Middle a,p, reflection (p,a) by GTARSKI3:def 13;
Collinear p, reflection (p,a),a by A7;
then a in Line (p,(reflection (p,a))) ;
hence between a,A, reflection (p,a) by A4, A1, A7, GTARSKI3:82, GTARSKI3:83, A2, A3, A6; :: thesis: verum