let AS be AffinSpace; for a, b, a9, b9, p being Element of AS
for M, N, P, Q being Subset of AS st p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & 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, p be Element of AS; for M, N, P, Q being Subset of AS st p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & 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; ( p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & 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:
p in M
and
A2:
a in M
and
A3:
b in M
and
A4:
p in N
and
A5:
a9 in N
and
A6:
b9 in N
and
A7:
not p in P
and
A8:
not p in Q
and
A9:
M <> N
and
A10:
a in P
and
A11:
a9 in P
and
A12:
b in Q
and
A13:
b9 in Q
and
A14:
M is being_line
and
A15:
N is being_line
and
A16:
P is being_line
and
A17:
Q is being_line
; ( P // Q or ex q being Element of AS st
( q in P & q in Q ) )
A18:
a <> a9
by A1, A2, A4, A5, A7, A9, A10, A14, A15, AFF_1:18;
LIN p,a,b
by A1, A2, A3, A14, AFF_1:21;
then consider c being Element of AS such that
A19:
LIN p,a9,c
and
A20:
a,a9 // b,c
by A7, A10, Th1;
set D = Line (b,c);
A21:
b in Line (b,c)
by AFF_1:15;
A22:
c in Line (b,c)
by AFF_1:15;
A23:
b <> b9
by A1, A3, A4, A6, A8, A9, A12, A14, A15, AFF_1:18;
A24:
c in N
by A4, A5, A7, A11, A15, A19, AFF_1:25;
then A25:
b <> c
by A1, A3, A4, A8, A9, A12, A14, A15, AFF_1:18;
then A26:
Line (b,c) is being_line
by AFF_1:def 3;
now ( Line (b,c) <> Q implies ex q being Element of AS st
( q in P & q in Q ) )assume
Line (
b,
c)
<> Q
;
ex q being Element of AS st
( q in P & q in Q )then A27:
c <> b9
by A12, A13, A17, A23, A26, A21, A22, AFF_1:18;
LIN b9,
c,
a9
by A5, A6, A15, A24, AFF_1:21;
then consider q being
Element of
AS such that A28:
LIN b9,
b,
q
and A29:
c,
b // a9,
q
by A27, Th1;
a9,
a // c,
b
by A20, AFF_1:4;
then
a9,
a // a9,
q
by A25, A29, AFF_1:5;
then
LIN a9,
a,
q
by AFF_1:def 1;
then A30:
q in P
by A10, A11, A16, A18, AFF_1:25;
q in Q
by A12, A13, A17, A23, A28, AFF_1:25;
hence
ex
q being
Element of
AS st
(
q in P &
q in Q )
by A30;
verum end;
hence
( P // Q or ex q being Element of AS st
( q in P & q in Q ) )
by A10, A11, A12, A16, A17, A18, A20, A25, A22, AFF_1:38; verum