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_plane & not a in A holds
ex c being POINT of S st between2 a,A,c
let a be POINT of S; :: thesis: for A being Subset of S st A is_plane & not a in A holds
ex c being POINT of S st between2 a,A,c
let A be Subset of S; :: thesis: ( A is_plane & not a in A implies ex c being POINT of S st between2 a,A,c )
assume that
A1: A is_plane and
A2: not a in A ; :: thesis: ex c being POINT of S st between2 a,A,c
consider p, q, r being POINT of S such that
A3: not Collinear p,q,r and
A4: A = Plane (p,q,r) by A1;
A5: not r in Line (p,q)

proof

assume r in Line (p,q) ; :: thesis: contradiction
then ex x being POINT of S st
( r = x & Collinear p,q,x ) ;
hence contradiction by A3; :: thesis: verum

end;

p <> q by A3, GTARSKI3:46;
then A6: ( A = Plane ((Line (p,q)),r) & Line (p,q) is_line ) by A3, Def11, A4;
then Line (p,q) c= A by A5, Th31;
then A7: ( p in A & q in A & r in A ) by A5, Th31, A6, GTARSKI3:83;
set c = reflection (p,a);
A8: 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, A7, GTARSKI3:104, GTARSKI1:def 7; :: thesis: verum

end;

take reflection (p,a) ; :: thesis: between2 a,A, reflection (p,a)
A9: Middle a,p, reflection (p,a) by GTARSKI3:def 13;
Collinear p, reflection (p,a),a by A9;
then A10: a in Line (p,(reflection (p,a))) ;
not reflection (p,a) in A

proof

assume reflection (p,a) in A ; :: thesis: contradiction
then Line (p,(reflection (p,a))) c= A by A7, A3, A8, A4, Th69;
hence contradiction by A10, A2; :: thesis: verum

end;

hence between2 a,A, reflection (p,a) by A9, A1, A2, A7; :: thesis: verum