let AS be AffinSpace; :: thesis: for a being Element of AS
for X being Subset of AS st X is being_plane holds
ex Y being Subset of AS st
( a in Y & X '||' Y & Y is being_plane )
let a be Element of AS; :: thesis: for X being Subset of AS st X is being_plane holds
ex Y being Subset of AS st
( a in Y & X '||' Y & Y is being_plane )
let X be Subset of AS; :: thesis: ( X is being_plane implies ex Y being Subset of AS st
( a in Y & X '||' Y & Y is being_plane ) )
assume A1: X is being_plane ; :: thesis: ex Y being Subset of AS st
( a in Y & X '||' Y & Y is being_plane )
then consider p, q, r being Element of AS such that
A2: p in X and
A3: q in X and
A4: r in X and
A5: not LIN p,q,r by Th34;
set M = Line p,q;
set N = Line p,r;
A6: p <> r by A5, AFF_1:16;
then A7: Line p,r c= X by A1, A2, A4, Th19;
set M9 = a * (Line p,q);
set N9 = a * (Line p,r);
A8: p <> q by A5, AFF_1:16;
then A9: Line p,q is being_line by AFF_1:def 3;
then A10: a * (Line p,q) is being_line by Th27;
A11: ( p in Line p,r & r in Line p,r ) by AFF_1:26;
A12: p in Line p,q by AFF_1:26;
A13: q in Line p,q by AFF_1:26;
A14: not Line p,q // Line p,r

proof

assume Line p,q // Line p,r ; :: thesis: contradiction
then r in Line p,q by A12, A11, AFF_1:59;
hence contradiction by A5, A12, A13, A9, AFF_1:33; :: thesis: verum

end;

A15: Line p,r is being_line by A6, AFF_1:def 3;
then A16: Line p,r // a * (Line p,r) by Def3;
A17: Line p,q // a * (Line p,q) by A9, Def3;
A18: a in a * (Line p,q) by A9, Def3;
( a * (Line p,r) is being_line & a in a * (Line p,r) ) by A15, Def3, Th27;
then consider Y being Subset of AS such that
A19: a * (Line p,q) c= Y and
A20: a * (Line p,r) c= Y and
A21: Y is being_plane by A10, A18, Th38;
Line p,q c= X by A1, A2, A3, A8, Th19;
then X '||' Y by A1, A17, A16, A19, A20, A21, A7, A14, Th55;
hence ex Y being Subset of AS st
( a in Y & X '||' Y & Y is being_plane ) by A18, A19, A21; :: thesis: verum