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, Th50;
assume A5: 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);
A6: len g in dom g by FINSEQ_5:6;
then A7: g . (len g) = g /. (len g) by PARTFUN1:def 6;
A8: 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 A9: NW-corner (L~ f) in (L~ g) /\ (L~ f) by A3, A5, JORDAN5C:def 2;
then A10: NW-corner (L~ f) in L~ g by XBOOLE_0:def 4;
then A11: 1 <= Index ((NW-corner (L~ f)),g) by JORDAN3:8;
A12: NW-corner (L~ f) in LSeg (g,(Index ((NW-corner (L~ f)),g))) by A10, JORDAN3:9;
A13: Index ((NW-corner (L~ f)),g) < len g by A10, JORDAN3:8;
then A14: (Index ((NW-corner (L~ f)),g)) + 1 <= len g by NAT_1:13;
then A15: (Index ((NW-corner (L~ f)),g)) + 1 in dom g by A8, FINSEQ_3:25;
A16: L~ f misses RightComp f by Th42;

A17: now

A18: len g >= 1 by A14, A8, XXREAL_0:2;
assume NW-corner (L~ f) <> g . ((Index ((NW-corner (L~ f)),g)) + 1) ; :: thesis: contradiction
then A19: NW-corner (L~ f) <> g /. ((Index ((NW-corner (L~ f)),g)) + 1) by A15, 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 A20: 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, A16, XBOOLE_0:3;
then (Index ((NW-corner (L~ f)),g)) + 1 < len g by A14, XXREAL_0:1;
then A21: ((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 A8, TOPREAL1:21;
then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A3, A5, A11, A14, A12, A8, A19, A20, A21, JORDAN5C:28;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

suppose A22: not g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ; :: thesis: contradiction

A23: now

assume A24: 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 Th54;
then A25: 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 A24;
A26: ( 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 A11, A14, 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 A12, A26, SPPOL_1:40, SPPOL_1:41;
hence contradiction by A25, 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, A14, A8, A18, JORDAN3:6;
A27: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A2, A14, A23, XXREAL_0:1;
g /. ((Index ((NW-corner (L~ f)),g)) + 1) in (L~ f) ` by A22, 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 A23, XBOOLE_0:def 3;
then A28: m /. 1 in LeftComp f by A6, A15, SPRECT_2:8;
m /. (len m) in RightComp f by A2, A6, A15, SPRECT_2:9;
then L~ f meets L~ m by A28, Th50;
then consider q being set such that
A29: q in L~ f and
A30: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A30;
consider i being Element of NAT such that
A31: 1 <= i and
A32: i + 1 <= len m and
A33: q in LSeg (m,i) by A30, SPPOL_2:13;
set j = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1;
A34: (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 ;
A35: len m = ((len g) -' ((Index ((NW-corner (L~ f)),g)) + 1)) + 1 by A14, A8, JORDAN4:8;
then len m = (len g) -' (Index ((NW-corner (L~ f)),g)) by A10, JORDAN3:8, NAT_2:7;
then (len m) + (Index ((NW-corner (L~ f)),g)) = len g by A13, XREAL_1:235;
then (i + 1) + (Index ((NW-corner (L~ f)),g)) <= len g by A32, XREAL_1:6;
then A36: ((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1) + 1 <= len g by A34;
i < len m by A32, NAT_1:13;
then A37: LSeg (m,i) = LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1)) by A8, A27, A31, A35, JORDAN4:19;
A38: (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 >= (Index ((NW-corner (L~ f)),g)) + 1 by A31, A34, XREAL_1:6;

A39: now

assume NW-corner (L~ f) = q ; :: thesis: contradiction
then A40: 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 A12, A33, A37, XBOOLE_0:def 4;
then A41: LSeg (g,(Index ((NW-corner (L~ f)),g))) meets LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1)) by XBOOLE_0:4;

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 A38, XXREAL_0:1;

suppose A42: (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 A27, 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 A11, TOPREAL1:def 6;
hence contradiction by A19, A40, A42, 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 A41, TOPREAL1:def 7; :: thesis: verum

end;

end;

end;

Index ((NW-corner (L~ f)),g) >= 0 by NAT_1:2;
then 0 + 1 <= (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 by A31, A34, XREAL_1:7;
then Index ((NW-corner (L~ f)),g) >= (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 by A3, A5, A11, A14, A12, A29, A33, A37, A36, A39, JORDAN5C:28;
then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A38, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

end;

end;

NW-corner (L~ f) in L~ f by A9, XBOOLE_0:def 4;
then NW-corner (L~ f) <> g . (len g) by A2, A16, A7, XBOOLE_0:3;
then A43: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A14, A17, XXREAL_0:1;
then A44: ((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 A8, TOPREAL1:21;
then A45: NW-corner (L~ f) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A15, A17, PARTFUN1:def 6;
A46: 1 <= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:11;
then A47: len g >= 1 by A44, XXREAL_0:2;
A48: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 in dom g by A44, A46, FINSEQ_3:25;
(Index ((NW-corner (L~ f)),g)) + 1 < ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:13;
then A49: NW-corner (L~ f) <> g . (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A15, A17, A48, FUNCT_1:def 4;
then A50: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A48, 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 A51: g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ; :: thesis: contradiction

A52: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A48, A49, PARTFUN1:def 6;
((Index ((NW-corner (L~ f)),g)) + 1) + 1 <> len g by A2, A16, A51, XBOOLE_0:3;
then ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A44, XXREAL_0:1;
then A53: (((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 A46, TOPREAL1:21;
then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A3, A5, A8, A44, A46, A45, A51, A53, A52, JORDAN5C:28;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

suppose A54: not g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ; :: thesis: contradiction

A55: now

assume A56: 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 Th54;
then A57: 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 A56;
A58: ( 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 A8, A44, 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 A45, A58, SPPOL_1:40, SPPOL_1:41;
hence contradiction by A57, 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, A44, A46, A47, JORDAN3:6;
A59: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A2, A44, A55, XXREAL_0:1;
g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in (L~ f) ` by A54, 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 A55, XBOOLE_0:def 3;
then A60: m /. 1 in LeftComp f by A6, A48, SPRECT_2:8;
m /. (len m) in RightComp f by A2, A6, A48, SPRECT_2:9;
then L~ f meets L~ m by A60, Th50;
then consider q being set such that
A61: q in L~ f and
A62: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A62;
consider i being Element of NAT such that
A63: 1 <= i and
A64: i + 1 <= len m and
A65: q in LSeg (m,i) by A62, SPPOL_2:13;
set j = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1;
A66: len m = ((len g) -' (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) + 1 by A44, A46, JORDAN4:8;
then len m = (len g) -' ((Index ((NW-corner (L~ f)),g)) + 1) by A43, NAT_2:7;
then (len m) + ((Index ((NW-corner (L~ f)),g)) + 1) = len g by A14, XREAL_1:235;
then (i + 1) + ((Index ((NW-corner (L~ f)),g)) + 1) <= len g by A64, XREAL_1:6;
then A67: ((i + 1) + (Index ((NW-corner (L~ f)),g))) + 1 <= len g ;
i < len m by A64, NAT_1:13;
then A68: LSeg (m,i) = LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1)) by A46, A59, A63, A66, JORDAN4:19;
A69: (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 A70: (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A63, XREAL_1:6;

A71: now

assume NW-corner (L~ f) = q ; :: thesis: contradiction
then A72: 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 A45, A65, A68, XBOOLE_0:def 4;
then A73: LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) meets LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1)) by XBOOLE_0:4;

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 A70, XXREAL_0:1;

suppose A74: ((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 A59, 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 A8, TOPREAL1:def 6;
hence contradiction by A50, A72, A74, 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 A73, TOPREAL1:def 7; :: thesis: verum

end;

end;

end;

0 + 1 <= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A69, NAT_1:11;
then (Index ((NW-corner (L~ f)),g)) + 1 >= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A3, A5, A8, A44, A45, A61, A65, A68, A69, A67, A71, JORDAN5C:28;
then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A70, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

end;