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