let f be rectangular special_circular_sequence; :: thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f)
let g be S-Sequence_in_R2; :: thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f) )
assume that
A1: g /. 1 in LeftComp f and
A2: g /. (len g) in RightComp f ; :: thesis: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f)
A3: L~ f meets L~ g by A1, A2, Th33;
assume A4: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = NW-corner (L~ f) ; :: thesis: contradiction
set nw = NW-corner (L~ f);
set inw = Index ((NW-corner (L~ f)),g);
A5: len g in dom g by FINSEQ_5:6;
then A6: g . (len g) = g /. (len g) by PARTFUN1:def 6;
A7: 1 <= (Index ((NW-corner (L~ f)),g)) + 1 by NAT_1:11;
L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25;
then A8: NW-corner (L~ f) in (L~ g) /\ (L~ f) by A3, A4, JORDAN5C:def 2;
then A9: NW-corner (L~ f) in L~ g by XBOOLE_0:def 4;
then A10: 1 <= Index ((NW-corner (L~ f)),g) by JORDAN3:8;
A11: NW-corner (L~ f) in LSeg (g,(Index ((NW-corner (L~ f)),g))) by A9, JORDAN3:9;
A12: Index ((NW-corner (L~ f)),g) < len g by A9, JORDAN3:8;
then A13: (Index ((NW-corner (L~ f)),g)) + 1 <= len g by NAT_1:13;
then A14: (Index ((NW-corner (L~ f)),g)) + 1 in dom g by A7, FINSEQ_3:25;
A15: L~ f misses RightComp f by Th25;
A16: now :: thesis: not NW-corner (L~ f) <> g . ((Index ((NW-corner (L~ f)),g)) + 1)
A17: len g >= 1 by A13, A7, XXREAL_0:2;
assume NW-corner (L~ f) <> g . ((Index ((NW-corner (L~ f)),g)) + 1) ; :: thesis: contradiction
then A18: NW-corner (L~ f) <> g /. ((Index ((NW-corner (L~ f)),g)) + 1) by A14, PARTFUN1:def 6;
per cases ( g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f or not g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ) ;
suppose A19: g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ; :: thesis: contradiction
then (Index ((NW-corner (L~ f)),g)) + 1 <> len g by A2, A15, XBOOLE_0:3;
then (Index ((NW-corner (L~ f)),g)) + 1 < len g by A13, XXREAL_0:1;
then A20: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21;
then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A3, A4, A10, A13, A11, A7, A18, A19, A20, JORDAN5C:28;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
suppose A21: not g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ; :: thesis: contradiction
A22: now :: thesis: not g /. ((Index ((NW-corner (L~ f)),g)) + 1) in RightComp f
assume A23: g /. ((Index ((NW-corner (L~ f)),g)) + 1) in RightComp f ; :: thesis: contradiction
RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37;
then A24: ex q being Point of (TOP-REAL 2) st
( g /. ((Index ((NW-corner (L~ f)),g)) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A23;
A25: ( LSeg (g,(Index ((NW-corner (L~ f)),g))) is vertical or LSeg (g,(Index ((NW-corner (L~ f)),g))) is horizontal ) by SPPOL_1:19;
LSeg (g,(Index ((NW-corner (L~ f)),g))) = LSeg ((g /. (Index ((NW-corner (L~ f)),g))),(g /. ((Index ((NW-corner (L~ f)),g)) + 1))) by A10, A13, TOPREAL1:def 3;
then ( (g /. ((Index ((NW-corner (L~ f)),g)) + 1)) `1 = (NW-corner (L~ f)) `1 or (g /. ((Index ((NW-corner (L~ f)),g)) + 1)) `2 = (NW-corner (L~ f)) `2 ) by A11, A25, SPPOL_1:40, SPPOL_1:41;
hence contradiction by A24, EUCLID:52; :: thesis: verum
end;
then reconsider m = mid (g,((Index ((NW-corner (L~ f)),g)) + 1),(len g)) as S-Sequence_in_R2 by A2, A13, A7, A17, JORDAN3:6;
A26: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A2, A13, A22, XXREAL_0:1;
g /. ((Index ((NW-corner (L~ f)),g)) + 1) in (L~ f) ` by A21, SUBSET_1:29;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LeftComp f by A22, XBOOLE_0:def 3;
then A27: m /. 1 in LeftComp f by A5, A14, SPRECT_2:8;
m /. (len m) in RightComp f by A2, A5, A14, SPRECT_2:9;
then L~ f meets L~ m by A27, Th33;
then consider q being object such that
A28: q in L~ f and
A29: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A29;
consider i being Nat such that
A30: 1 <= i and
A31: i + 1 <= len m and
A32: q in LSeg (m,i) by A29, SPPOL_2:13;
set j = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1;
A33: (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 = ((i + (Index ((NW-corner (L~ f)),g))) + 1) -' 1
.= i + (Index ((NW-corner (L~ f)),g)) by NAT_D:34 ;
A34: len m = ((len g) -' ((Index ((NW-corner (L~ f)),g)) + 1)) + 1 by A13, A7, JORDAN4:8;
then len m = (len g) -' (Index ((NW-corner (L~ f)),g)) by A9, JORDAN3:8, NAT_2:7;
then (len m) + (Index ((NW-corner (L~ f)),g)) = len g by A12, XREAL_1:235;
then (i + 1) + (Index ((NW-corner (L~ f)),g)) <= len g by A31, XREAL_1:6;
then A35: ((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1) + 1 <= len g by A33;
i < len m by A31, NAT_1:13;
then A36: LSeg (m,i) = LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1)) by A7, A26, A30, A34, JORDAN4:19;
A37: (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 >= (Index ((NW-corner (L~ f)),g)) + 1 by A30, A33, XREAL_1:6;
A38: now :: thesis: not NW-corner (L~ f) = q
assume NW-corner (L~ f) = q ; :: thesis: contradiction
then A39: NW-corner (L~ f) in (LSeg (g,(Index ((NW-corner (L~ f)),g)))) /\ (LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1))) by A11, A32, A36, XBOOLE_0:def 4;
then A40: LSeg (g,(Index ((NW-corner (L~ f)),g))) meets LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1)) ;
per cases ( (Index ((NW-corner (L~ f)),g)) + 1 = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 or (Index ((NW-corner (L~ f)),g)) + 1 < (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 ) by A37, XXREAL_0:1;
suppose A41: (Index ((NW-corner (L~ f)),g)) + 1 = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 ; :: thesis: contradiction
((Index ((NW-corner (L~ f)),g)) + 1) + 1 <= len g by A26, NAT_1:13;
then (Index ((NW-corner (L~ f)),g)) + (1 + 1) <= len g ;
then (LSeg (g,(Index ((NW-corner (L~ f)),g)))) /\ (LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1))) = {(g /. ((Index ((NW-corner (L~ f)),g)) + 1))} by A10, TOPREAL1:def 6;
hence contradiction by A18, A39, A41, TARSKI:def 1; :: thesis: verum
end;
suppose (Index ((NW-corner (L~ f)),g)) + 1 < (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 ; :: thesis: contradiction
hence contradiction by A40, TOPREAL1:def 7; :: thesis: verum
end;
end;
end;
0 + 1 <= (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 by A30, A33, XREAL_1:7;
then Index ((NW-corner (L~ f)),g) >= (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 by A3, A4, A10, A13, A11, A28, A32, A36, A35, A38, JORDAN5C:28;
then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A37, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
end;
end;
NW-corner (L~ f) in L~ f by A8, XBOOLE_0:def 4;
then NW-corner (L~ f) <> g . (len g) by A2, A15, A6, XBOOLE_0:3;
then A42: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A13, A16, XXREAL_0:1;
then A43: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21;
then A44: NW-corner (L~ f) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A14, A16, PARTFUN1:def 6;
A45: 1 <= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:11;
then A46: len g >= 1 by A43, XXREAL_0:2;
A47: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 in dom g by A43, A45, FINSEQ_3:25;
(Index ((NW-corner (L~ f)),g)) + 1 < ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:13;
then A48: NW-corner (L~ f) <> g . (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A14, A16, A47, FUNCT_1:def 4;
then A49: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A47, PARTFUN1:def 6;
per cases ( g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f or not g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ) ;
suppose A50: g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ; :: thesis: contradiction
A51: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A47, A48, PARTFUN1:def 6;
((Index ((NW-corner (L~ f)),g)) + 1) + 1 <> len g by A2, A15, A50, XBOOLE_0:3;
then ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A43, XXREAL_0:1;
then A52: (((Index ((NW-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by NAT_1:13;
then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in LSeg (g,(((Index ((NW-corner (L~ f)),g)) + 1) + 1)) by A45, TOPREAL1:21;
then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A3, A4, A7, A43, A45, A44, A50, A52, A51, JORDAN5C:28;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
suppose A53: not g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ; :: thesis: contradiction
A54: now :: thesis: not g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in RightComp f
assume A55: g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in RightComp f ; :: thesis: contradiction
RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37;
then A56: ex q being Point of (TOP-REAL 2) st
( g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A55;
A57: ( LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) is vertical or LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) is horizontal ) by SPPOL_1:19;
LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) = LSeg ((g /. ((Index ((NW-corner (L~ f)),g)) + 1)),(g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1))) by A7, A43, TOPREAL1:def 3;
then ( (g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) `1 = (NW-corner (L~ f)) `1 or (g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) `2 = (NW-corner (L~ f)) `2 ) by A44, A57, SPPOL_1:40, SPPOL_1:41;
hence contradiction by A56, EUCLID:52; :: thesis: verum
end;
then reconsider m = mid (g,(((Index ((NW-corner (L~ f)),g)) + 1) + 1),(len g)) as S-Sequence_in_R2 by A2, A43, A45, A46, JORDAN3:6;
A58: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A2, A43, A54, XXREAL_0:1;
g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in (L~ f) ` by A53, SUBSET_1:29;
then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in LeftComp f by A54, XBOOLE_0:def 3;
then A59: m /. 1 in LeftComp f by A5, A47, SPRECT_2:8;
m /. (len m) in RightComp f by A2, A5, A47, SPRECT_2:9;
then L~ f meets L~ m by A59, Th33;
then consider q being object such that
A60: q in L~ f and
A61: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A61;
consider i being Nat such that
A62: 1 <= i and
A63: i + 1 <= len m and
A64: q in LSeg (m,i) by A61, SPPOL_2:13;
set j = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1;
A65: len m = ((len g) -' (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) + 1 by A43, A45, JORDAN4:8;
then len m = (len g) -' ((Index ((NW-corner (L~ f)),g)) + 1) by A42, NAT_2:7;
then (len m) + ((Index ((NW-corner (L~ f)),g)) + 1) = len g by A13, XREAL_1:235;
then (i + 1) + ((Index ((NW-corner (L~ f)),g)) + 1) <= len g by A63, XREAL_1:6;
then A66: ((i + 1) + (Index ((NW-corner (L~ f)),g))) + 1 <= len g ;
i < len m by A63, NAT_1:13;
then A67: LSeg (m,i) = LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1)) by A45, A58, A62, A65, JORDAN4:19;
A68: (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 = (((i + (Index ((NW-corner (L~ f)),g))) + 1) + 1) -' 1
.= (i + (Index ((NW-corner (L~ f)),g))) + 1 by NAT_D:34 ;
then (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 = i + ((Index ((NW-corner (L~ f)),g)) + 1) ;
then A69: (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A62, XREAL_1:6;
A70: now :: thesis: not NW-corner (L~ f) = q
assume NW-corner (L~ f) = q ; :: thesis: contradiction
then A71: NW-corner (L~ f) in (LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1))) /\ (LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1))) by A44, A64, A67, XBOOLE_0:def 4;
then A72: LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) meets LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1)) ;
per cases ( ((Index ((NW-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 or ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 ) by A69, XXREAL_0:1;
suppose A73: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 ; :: thesis: contradiction
(((Index ((NW-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by A58, NAT_1:13;
then ((Index ((NW-corner (L~ f)),g)) + 1) + (1 + 1) <= len g ;
then (LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1))) /\ (LSeg (g,(((Index ((NW-corner (L~ f)),g)) + 1) + 1))) = {(g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1))} by A7, TOPREAL1:def 6;
hence contradiction by A49, A71, A73, TARSKI:def 1; :: thesis: verum
end;
suppose ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 ; :: thesis: contradiction
hence contradiction by A72, TOPREAL1:def 7; :: thesis: verum
end;
end;
end;
0 + 1 <= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A68, NAT_1:11;
then (Index ((NW-corner (L~ f)),g)) + 1 >= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A3, A4, A7, A43, A44, A60, A64, A67, A68, A66, A70, JORDAN5C:28;
then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A69, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
end;