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)

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

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

A16:
Line (a,c) is being_line
by A10, AFF_1:def 3;
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;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

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