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:45;
A14:
N is being_line
by A10, AFF_1:36;
A15:
b <> b9
by A2, A4, A9, A10, AFF_1:45;
A16:
M is being_line
by A10, AFF_1:36;
now ( a <> b & not P // Q implies ex q being Element of AS st
( q in P & q in Q ) )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:40;
set D =
Line (
b,
c);
A20:
b in Line (
b,
c)
by AFF_1:15;
A21:
c in Line (
b,
c)
by AFF_1:15;
a,
b // N
by A1, A2, A10, A16, AFF_1:43, AFF_1:52;
then
a9,
c // N
by A17, A18, AFF_1:32;
then A22:
c in N
by A3, A14, AFF_1:23;
then A23:
b <> c
by A2, A9, A10, AFF_1:45;
then A24:
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 A25:
c <> b9
by A7, A8, A12, A15, A24, A20, A21, AFF_1:18;
LIN b9,
c,
a9
by A3, A4, A14, A22, AFF_1:21;
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:4;
then
a9,
a // a9,
q
by A23, A27, AFF_1:5;
then
LIN a9,
a,
q
by AFF_1:def 1;
then A28:
q in P
by A5, A6, A11, A13, AFF_1:25;
q in Q
by A7, A8, A12, A15, A26, AFF_1:25;
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:38;
verum end;
hence
( P // Q or ex q being Element of AS st
( q in P & q in Q ) )
by A5, A7; verum