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)

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

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

A15:
Line (p,r) is being_line
by A6, AFF_1:def 3;
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;then r in Line (p,q) by A12, A11, AFF_1:45;

hence contradiction by A5, A12, A13, A9, AFF_1:21; :: thesis: verum

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