let P1, P2 be Subset of (TOP-REAL 2); for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 & p `1 <= q1 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P1 meets P2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ( P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 & p `1 <= q1 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 & p `2 <= q2 `2 ) ) implies P1 meets P2 )
assume that
A1:
P1 is_S-P_arc_joining p1,q1
and
A2:
P2 is_S-P_arc_joining p2,q2
and
A3:
for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 & p `1 <= q1 `1 )
and
A4:
for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 & p `2 <= q2 `2 )
; P1 meets P2
consider f1 being FinSequence of (TOP-REAL 2) such that
A5:
f1 is being_S-Seq
and
A6:
P1 = L~ f1
and
A7:
p1 = f1 /. 1
and
A8:
q1 = f1 /. (len f1)
by A1, TOPREAL4:def 1;
len f1 <> 0
by A5, TOPREAL1:def 8;
then reconsider f1 = f1 as non empty FinSequence of (TOP-REAL 2) ;
A9:
Seg (len f1) = dom f1
by FINSEQ_1:def 3;
consider f2 being FinSequence of (TOP-REAL 2) such that
A10:
f2 is being_S-Seq
and
A11:
P2 = L~ f2
and
A12:
p2 = f2 /. 1
and
A13:
q2 = f2 /. (len f2)
by A2, TOPREAL4:def 1;
len f2 <> 0
by A10, TOPREAL1:def 8;
then reconsider f2 = f2 as non empty FinSequence of (TOP-REAL 2) ;
A14:
Seg (len f2) = dom f2
by FINSEQ_1:def 3;
set x1 = X_axis f1;
set y1 = Y_axis f1;
set x2 = X_axis f2;
set y2 = Y_axis f2;
A15:
( Seg (len (X_axis f1)) = dom (X_axis f1) & len (X_axis f1) = len f1 )
by FINSEQ_1:def 3, GOBOARD1:def 1;
A16:
( dom (Y_axis f2) = Seg (len (Y_axis f2)) & len (Y_axis f2) = len f2 )
by FINSEQ_1:def 3, GOBOARD1:def 2;
A17:
2 <= len f2
by A10, TOPREAL1:def 8;
then A18:
1 <= len f2
by XXREAL_0:2;
then
1 in dom f2
by FINSEQ_3:25;
then A19:
(Y_axis f2) . 1 = p2 `2
by A12, A14, A16, GOBOARD1:def 2;
len f2 in dom f2
by A18, FINSEQ_3:25;
then A20:
(Y_axis f2) . (len f2) = q2 `2
by A13, A14, A16, GOBOARD1:def 2;
A21:
Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2)
A24:
2 <= len f1
by A5, TOPREAL1:def 8;
then A25:
1 <= len f1
by XXREAL_0:2;
then
1 in dom f1
by FINSEQ_3:25;
then A26:
(X_axis f1) . 1 = p1 `1
by A7, A9, A15, GOBOARD1:def 1;
len f1 in dom f1
by A25, FINSEQ_3:25;
then A27:
(X_axis f1) . (len f1) = q1 `1
by A8, A9, A15, GOBOARD1:def 1;
A28:
X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1)
A31:
( dom (X_axis f2) = Seg (len (X_axis f2)) & len (X_axis f2) = len f2 )
by FINSEQ_1:def 3, GOBOARD1:def 1;
A32:
X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1)
A35:
( dom (Y_axis f1) = Seg (len (Y_axis f1)) & len (Y_axis f1) = len f1 )
by FINSEQ_1:def 3, GOBOARD1:def 2;
A36:
Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2)
A39:
( f2 is one-to-one & f2 is special )
by A10, TOPREAL1:def 8;
( f1 is one-to-one & f1 is special )
by A5, TOPREAL1:def 8;
hence
P1 meets P2
by A6, A11, A39, A24, A17, A28, A32, A36, A21, Th5; verum