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 E being Subset of S st
( E is_plane & A c= E & A9 c= E & Plane (A,A9) = E )
let p be POINT of S; :: thesis: for A, A9 being Subset of S st A,A9 Is p holds
ex E being Subset of S st
( E is_plane & A c= E & A9 c= E & Plane (A,A9) = E )
let A, A9 be Subset of S; :: thesis: ( A,A9 Is p implies ex E being Subset of S st
( E is_plane & A c= E & A9 c= E & Plane (A,A9) = E ) )
assume A1: A,A9 Is p ; :: thesis: ex E being Subset of S st
( E is_plane & A c= E & A9 c= E & Plane (A,A9) = E )
then p in A /\ A9 by XBOOLE_0:def 4;
then consider r being POINT of S such that
A2: not r in A and
r in A9 and
A3: Plane (A,A9) = Plane (A,r) by A1, Def13;
consider E being Subset of S such that
A4: E is_plane and
A c= E and
r in E and
A5: Plane (A,r) = E by A1, A2, Th50;
take E ; :: thesis: ( E is_plane & A c= E & A9 c= E & Plane (A,A9) = E )
thus ( E is_plane & A c= E & A9 c= E & Plane (A,A9) = E ) by A1, A3, A4, A5, Th43; :: thesis: verum