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:7;
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:7;
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:15;
A12: p in Line (p,q) by AFF_1:15;
A13: q in Line (p,q) by AFF_1:15;
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:45;
hence contradiction by A5, A12, A13, A9, AFF_1:21; :: 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