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

proof

assume Line (a,b) = Line (a,c) ; :: thesis: contradiction
then A15: c in Line (a,b) by AFF_1:15;
( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;
hence contradiction by A9, A13, A15, AFF_1:21; :: thesis: verum

end;

A16: Line (a,c) is being_line by A10, AFF_1:def 3;
then ( a in Line (a,c) & a * (Line (a,c)) c= Y ) by A3, A6, A11, AFF_1:15;
then A17: Line (a,c) c= Y by A16, Lm8;
A18: Line (a,b) c= X by A1, A5, A7, A12, Th19;
then ( a in Line (a,b) & a * (Line (a,b)) c= Y ) by A3, A6, A13, AFF_1:15;
then Line (a,b) c= Y by A13, Lm8;
hence contradiction by A1, A2, A4, A13, A16, A18, A11, A17, A14, Th26; :: thesis: verum