let AS be AffinSpace; 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; ( 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
; 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 )
; 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)
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; verum