let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for c being POINT of S
for A being Subset of S st A is_line & not c in A holds
ex E being Subset of S st
( E is_plane & A c= E & c in E & Plane (A,c) = E )
let c be POINT of S; :: thesis: for A being Subset of S st A is_line & not c in A holds
ex E being Subset of S st
( E is_plane & A c= E & c in E & Plane (A,c) = E )
let A be Subset of S; :: thesis: ( A is_line & not c in A implies ex E being Subset of S st
( E is_plane & A c= E & c in E & Plane (A,c) = E ) )
assume that
A1: A is_line and
A2: not c in A ; :: thesis: ex E being Subset of S st
( E is_plane & A c= E & c in E & Plane (A,c) = E )
consider a, b being POINT of S such that
a <> b and
A3: A = Line (a,b) by A1;
set E = Plane (A,c);
A4: not Collinear a,b,c by A2, A3;
then Plane (A,c) = Plane (a,b,c) by A3, Def11;
then U1: Plane (A,c) is_plane by A4;
U2: A c= Plane (A,c) by A1, A2, Th31;
c in Plane (A,c) by A1, A2, Th48;
hence ex E being Subset of S st
( E is_plane & A c= E & c in E & Plane (A,c) = E ) by U1, U2; :: thesis: verum