let AS be AffinSpace; for A, K, X, Y being Subset of AS st not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is being_line & K is being_line & X is being_plane & Y is being_plane holds
X '||' Y
let A, K, X, Y be Subset of AS; ( not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is being_line & K is being_line & X is being_plane & Y is being_plane implies X '||' Y )
assume that
A1:
not A // K
and
A2:
A '||' X
and
A3:
A '||' Y
and
A4:
K '||' X
and
A5:
K '||' Y
and
A6:
A is being_line
and
A7:
K is being_line
and
A8:
X is being_plane
and
A9:
Y is being_plane
; X '||' Y
set y = the Element of Y;
set x = the Element of X;
A10:
Y <> {}
by A9, AFF_4:59;
A11:
X <> {}
by A8, AFF_4:59;
then reconsider a = the Element of X, b = the Element of Y as Element of AS by A10, TARSKI:def 3;
A12:
K // a * K
by A7, AFF_4:def 3;
A13:
A // a * A
by A6, AFF_4:def 3;
A14:
not a * A // a * K
a * K c= a + X
by A4, A7, A8, AFF_4:68;
then A15:
a * K c= X
by A8, A11, AFF_4:66;
K // b * K
by A7, AFF_4:def 3;
then A16:
a * K // b * K
by A12, AFF_1:44;
b * A c= b + Y
by A3, A6, A9, AFF_4:68;
then A17:
b * A c= Y
by A9, A10, AFF_4:66;
A // b * A
by A6, AFF_4:def 3;
then A18:
a * A // b * A
by A13, AFF_1:44;
b * K c= b + Y
by A5, A7, A9, AFF_4:68;
then A19:
b * K c= Y
by A9, A10, AFF_4:66;
a * A c= a + X
by A2, A6, A8, AFF_4:68;
then
a * A c= X
by A8, A11, AFF_4:66;
hence
X '||' Y
by A8, A9, A15, A17, A19, A14, A18, A16, AFF_4:55; verum