let AS be AffinSpace; for a, b, a9, b9 being Element of AS
for M, N, P, Q being Subset of AS st a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & P is being_line & Q is being_line & not P // Q holds
ex q being Element of AS st
( q in P & q in Q )
let a, b, a9, b9 be Element of AS; for M, N, P, Q being Subset of AS st a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & P is being_line & Q is being_line & not P // Q holds
ex q being Element of AS st
( q in P & q in Q )
let M, N, P, Q be Subset of AS; ( a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & P is being_line & Q is being_line & not P // Q implies ex q being Element of AS st
( q in P & q in Q ) )
assume that
A1:
a in M
and
A2:
b in M
and
A3:
a9 in N
and
A4:
b9 in N
and
A5:
a in P
and
A6:
a9 in P
and
A7:
b in Q
and
A8:
b9 in Q
and
A9:
M <> N
and
A10:
M // N
and
A11:
P is being_line
and
A12:
Q is being_line
; ( P // Q or ex q being Element of AS st
( q in P & q in Q ) )
A13:
a <> a9
by A1, A3, A9, A10, AFF_1:59;
A14:
N is being_line
by A10, AFF_1:50;
A15:
b <> b9
by A2, A4, A9, A10, AFF_1:59;
A16:
M is being_line
by A10, AFF_1:50;
now assume A17:
a <> b
;
( P // Q or ex q being Element of AS st
( q in P & q in Q ) )consider c being
Element of
AS such that A18:
a,
b // a9,
c
and A19:
a,
a9 // b,
c
by DIRAF:47;
set D =
Line b,
c;
A20:
b in Line b,
c
by AFF_1:26;
A21:
c in Line b,
c
by AFF_1:26;
a,
b // N
by A1, A2, A10, A16, AFF_1:57, AFF_1:66;
then
a9,
c // N
by A17, A18, AFF_1:46;
then A22:
c in N
by A3, A14, AFF_1:37;
then A23:
b <> c
by A2, A9, A10, AFF_1:59;
then A24:
Line b,
c is
being_line
by AFF_1:def 3;
now assume
Line b,
c <> Q
;
ex q being Element of AS st
( q in P & q in Q )then A25:
c <> b9
by A7, A8, A12, A15, A24, A20, A21, AFF_1:30;
LIN b9,
c,
a9
by A3, A4, A14, A22, AFF_1:33;
then consider q being
Element of
AS such that A26:
LIN b9,
b,
q
and A27:
c,
b // a9,
q
by A25, Th1;
a9,
a // c,
b
by A19, AFF_1:13;
then
a9,
a // a9,
q
by A23, A27, AFF_1:14;
then
LIN a9,
a,
q
by AFF_1:def 1;
then A28:
q in P
by A5, A6, A11, A13, AFF_1:39;
q in Q
by A7, A8, A12, A15, A26, AFF_1:39;
hence
ex
q being
Element of
AS st
(
q in P &
q in Q )
by A28;
verum end; hence
(
P // Q or ex
q being
Element of
AS st
(
q in P &
q in Q ) )
by A5, A6, A7, A11, A12, A13, A19, A23, A21, AFF_1:52;
verum end;
hence
( P // Q or ex q being Element of AS st
( q in P & q in Q ) )
by A5, A7; verum