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:16;
then A11:
Line a,c c= X
by A1, A5, A8, Th19;
A12:
a <> b
by A9, AFF_1:16;
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, Def4, AFF_1:26;
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, Def4, AFF_1:26;
then
Line a,b c= Y
by A13, Lm8;
hence
contradiction
by A1, A2, A4, A13, A16, A18, A11, A17, A14, Th26; verum