let AS be AffinSpace; 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; 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; ( 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
; 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;
now ( 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
;
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;
verum end;
hence
ex X being Subset of AS st
( a in X & A c= X & X is being_plane )
by A3; verum