let AS be AffinSpace; :: thesis: for a being Element of AS
for A being Subset of AS st A is being_line holds
ex X being Subset of AS st
( a in X & A c= X & X is being_plane )
let a be Element of AS; :: thesis: for A being Subset of AS st A is being_line holds
ex X being Subset of AS st
( a in X & A c= X & X is being_plane )
let A be Subset of AS; :: thesis: ( A is being_line implies ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) )
assume A1: A is being_line ; :: thesis: ex X being Subset of AS st
( a in X & A c= X & X is being_plane )
then consider p, q being Element of AS such that
A2: p in A and
q in A and
p <> q by AFF_1:19;

A3: now :: thesis: ( a in A implies ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) )

consider b being Element of AS such that
A4: not b in A by A1, Th12;
consider P being Subset of AS such that
A5: ( a in P & b in P ) and
A6: P is being_line by Th11;
set X = Plane (P,A);
A7: A c= Plane (P,A) by A6, Th14;
assume A8: a in A ; :: thesis: ex X being Subset of AS st
( a in X & A c= X & X is being_plane )
then not P // A by A4, A5, AFF_1:45;
then Plane (P,A) is being_plane by A1, A6;
hence ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) by A8, A7; :: thesis: verum

end;

now :: thesis: ( not a in A implies ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) )

consider P being Subset of AS such that
A9: a in P and
A10: p in P and
A11: P is being_line by Th11;
set X = Plane (P,A);
A c= Plane (P,A) by A11, Th14;
then A12: P c= Plane (P,A) by A2, A10, A11, Lm4, AFF_1:41;
assume not a in A ; :: thesis: ex X being Subset of AS st
( a in X & A c= X & X is being_plane )
then not P // A by A2, A9, A10, AFF_1:45;
then Plane (P,A) is being_plane by A1, A11;
hence ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) by A9, A11, A12, Th14; :: thesis: verum

end;

hence ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) by A3; :: thesis: verum