let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for p being POINT of S
for A, A9 being Subset of S st A,A9 Is p holds
ex r being POINT of S st
( not r in A & r in A9 & Plane (A,A9) = Plane (A,r) & A9 = Line (r,p) & ex r9 being POINT of S st
( between r,p,r9 & p <> r9 & Collinear r,p,r9 & not r9 in A & Plane (A,r) = Plane (A,r9) ) )
let p be POINT of S; :: thesis: for A, A9 being Subset of S st A,A9 Is p holds
ex r being POINT of S st
( not r in A & r in A9 & Plane (A,A9) = Plane (A,r) & A9 = Line (r,p) & ex r9 being POINT of S st
( between r,p,r9 & p <> r9 & Collinear r,p,r9 & not r9 in A & Plane (A,r) = Plane (A,r9) ) )
let A, A9 be Subset of S; :: thesis: ( A,A9 Is p implies ex r being POINT of S st
( not r in A & r in A9 & Plane (A,A9) = Plane (A,r) & A9 = Line (r,p) & ex r9 being POINT of S st
( between r,p,r9 & p <> r9 & Collinear r,p,r9 & not r9 in A & Plane (A,r) = Plane (A,r9) ) ) )
assume A1: A,A9 Is p ; :: thesis: ex r being POINT of S st
( not r in A & r in A9 & Plane (A,A9) = Plane (A,r) & A9 = Line (r,p) & ex r9 being POINT of S st
( between r,p,r9 & p <> r9 & Collinear r,p,r9 & not r9 in A & Plane (A,r) = Plane (A,r9) ) )
then ( A is_line & A9 is_line & A <> A9 & not A /\ A9 is empty ) by XBOOLE_0:def 4;
then consider r being POINT of S such that
A2: not r in A and
A3: r in A9 and
A4: Plane (A,A9) = Plane (A,r) by Def13;
A5: Line (r,p) = A9 by A1, A2, A3, GTARSKI3:87;
consider r9 being POINT of S such that
A6: between r,p,r9 and
A7: p <> r9 by GTARSKI3:36;
A8: Collinear r,p,r9 by A6;
A9: not r9 in A

proof

assume r9 in A ; :: thesis: contradiction
then ( A is_line & A9 is_line & A <> A9 & p in A & r9 in A & p in A9 & r9 in A9 ) by A8, A5, A1;
hence contradiction by A7, GTARSKI3:89; :: thesis: verum

end;

t3: ( r9 in A9 & A9 c= Plane (A,r) ) by A1, A2, A3, A5, A8, Th37;
Plane (A,r) = Plane (A,r9) by A9, Th34, A1, A2, t3;
hence ex r being POINT of S st
( not r in A & r in A9 & Plane (A,A9) = Plane (A,r) & A9 = Line (r,p) & ex r9 being POINT of S st
( between r,p,r9 & p <> r9 & Collinear r,p,r9 & not r9 in A & Plane (A,r) = Plane (A,r9) ) ) by A1, A2, A3, A4, A5, A6, A8, A9; :: thesis: verum