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;

( a in X & A c= X & X is being_plane ) by A3; :: thesis: verum

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 ) )

( 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;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

now :: thesis: ( not a in A implies ex X being Subset of AS st

( a in X & A c= X & X is being_plane ) )

hence
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;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

( a in X & A c= X & X is being_plane ) by A3; :: thesis: verum