let AS be AffinSpace; for a, b, a', b' being Element of
for M, N, P, Q being Subset of st a in M & b in M & a' in N & b' in N & a in P & a' in P & b in Q & b' in Q & M <> N & M // N & 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 a, b, a', b' be Element of ; for M, N, P, Q being Subset of st a in M & b in M & a' in N & b' in N & a in P & a' in P & b in Q & b' in Q & M <> N & M // N & 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 ; ( a in M & b in M & a' in N & b' in N & a in P & a' in P & b in Q & b' in Q & M <> N & M // N & 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:
a in M
and
A2:
b in M
and
A3:
a' in N
and
A4:
b' in N
and
A5:
a in P
and
A6:
a' in P
and
A7:
b in Q
and
A8:
b' 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 st
( q in P & q in Q ) )
A13:
a <> a'
by A1, A3, A9, A10, AFF_1:59;
A14:
N is being_line
by A10, AFF_1:50;
A15:
b <> b'
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 st
( q in P & q in Q ) )consider c being
Element of
such that A18:
a,
b // a',
c
and A19:
a,
a' // 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
a',
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 st
( q in P & q in Q )then A25:
c <> b'
by A7, A8, A12, A15, A24, A20, A21, AFF_1:30;
LIN b',
c,
a'
by A3, A4, A14, A22, AFF_1:33;
then consider q being
Element of
such that A26:
LIN b',
b,
q
and A27:
c,
b // a',
q
by A25, Th1;
a',
a // c,
b
by A19, AFF_1:13;
then
a',
a // a',
q
by A23, A27, AFF_1:14;
then
LIN a',
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 st
(
q in P &
q in Q )
by A28;
verum end; hence
(
P // Q or ex
q being
Element of 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 st
( q in P & q in Q ) )
by A5, A7; verum