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
( A c= Plane (A9,A) & A9 c= Plane (A,A9) )
let p be POINT of S; :: thesis: for A, A9 being Subset of S st A,A9 Is p holds
( A c= Plane (A9,A) & A9 c= Plane (A,A9) )
let A, A9 be Subset of S; :: thesis: ( A,A9 Is p implies ( A c= Plane (A9,A) & A9 c= Plane (A,A9) ) )
assume A1: A,A9 Is p ; :: thesis: ( A c= Plane (A9,A) & A9 c= Plane (A,A9) )
then A2: ( 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
A3: not r in A and
A4: r in A9 and
A5: Plane (A,A9) = Plane (A,r) by Def13;
consider s being POINT of S such that
A6: not s in A9 and
A7: s in A and
A8: Plane (A9,A) = Plane (A9,s) by A2, Def13;
( s <> p & A9,A Is p ) by A6, A1;
hence A c= Plane (A9,A) by A8, A7, Th37; :: thesis: A9 c= Plane (A,A9)
thus A9 c= Plane (A,A9) by A1, A3, A4, A5, Th37; :: thesis: verum