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

A19: now

A20: len g >= 1 by A16, A10, XXREAL_0:2;
assume NW-corner (L~ f) <> g . ((Index ((NW-corner (L~ f)),g)) + 1) ; :: thesis: contradiction
then A21: NW-corner (L~ f) <> g /. ((Index ((NW-corner (L~ f)),g)) + 1) by A17, PARTFUN1:def 8;

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 A22: 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, A18, XBOOLE_0:3;
then (Index ((NW-corner (L~ f)),g)) + 1 < len g by A16, XXREAL_0:1;
then A23: ((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 A10, TOPREAL1:27;
then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A3, A6, A13, A16, A14, A10, A21, A22, A23, JORDAN5C:28;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

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

A25: now

assume A26: 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 A27: 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 A26;
A28: ( LSeg (g,(Index ((NW-corner (L~ f)),g))) is vertical or LSeg (g,(Index ((NW-corner (L~ f)),g))) is horizontal ) by SPPOL_1:41;
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 A13, A16, TOPREAL1:def 5;
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 A14, A28, SPPOL_1:63, SPPOL_1:64;
hence contradiction by A27, EUCLID:56; :: thesis: verum

end;

then reconsider m = mid (g,((Index ((NW-corner (L~ f)),g)) + 1),(len g)) as S-Sequence_in_R2 by A2, A16, A10, A20, JORDAN3:39;
A29: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A2, A16, A25, XXREAL_0:1;
g /. ((Index ((NW-corner (L~ f)),g)) + 1) in (L~ f) ` by A24, SUBSET_1:50;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:11;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LeftComp f by A25, XBOOLE_0:def 3;
then A30: m /. 1 in LeftComp f by A8, A17, SPRECT_2:12;
m /. (len m) in RightComp f by A2, A8, A17, SPRECT_2:13;
then L~ f meets L~ m by A30, Th50;
then consider q being set such that
A31: q in L~ f and
A32: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A32;
consider i being Element of NAT such that
A33: 1 <= i and
A34: i + 1 <= len m and
A35: q in LSeg (m,i) by A32, SPPOL_2:13;
set j = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1;
A36: (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 ;
A37: len m = ((len g) -' ((Index ((NW-corner (L~ f)),g)) + 1)) + 1 by A16, A10, JORDAN4:20;
then len m = (len g) -' (Index ((NW-corner (L~ f)),g)) by A12, JORDAN3:41, NAT_2:9;
then (len m) + (Index ((NW-corner (L~ f)),g)) = len g by A15, XREAL_1:237;
then (i + 1) + (Index ((NW-corner (L~ f)),g)) <= len g by A34, XREAL_1:8;
then A38: ((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1) + 1 <= len g by A36;
i < len m by A34, NAT_1:13;
then A39: LSeg (m,i) = LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1)) by A10, A29, A33, A37, JORDAN4:31;
A40: (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 >= (Index ((NW-corner (L~ f)),g)) + 1 by A33, A36, XREAL_1:8;

A41: now

assume NW-corner (L~ f) = q ; :: thesis: contradiction
then A42: 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 A14, A35, A39, XBOOLE_0:def 4;
then A43: 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 A40, XXREAL_0:1;

suppose A44: (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 A29, 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 A13, TOPREAL1:def 8;
hence contradiction by A21, A42, A44, 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 A43, TOPREAL1:def 9; :: 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 A33, A36, XREAL_1:9;
then Index ((NW-corner (L~ f)),g) >= (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 by A3, A6, A13, A16, A14, A31, A35, A39, A38, A41, JORDAN5C:28;
then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A40, XXREAL_0:2;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

end;

end;

NW-corner (L~ f) in L~ f by A11, XBOOLE_0:def 4;
then NW-corner (L~ f) <> g . (len g) by A2, A18, A9, XBOOLE_0:3;
then A45: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A16, A19, XXREAL_0:1;
then A46: ((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 A10, TOPREAL1:27;
then A47: NW-corner (L~ f) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A17, A19, PARTFUN1:def 8;
A48: 1 <= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:11;
then A49: len g >= 1 by A46, XXREAL_0:2;
A50: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 in dom g by A46, A48, FINSEQ_3:27;
(Index ((NW-corner (L~ f)),g)) + 1 < ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:13;
then A51: NW-corner (L~ f) <> g . (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A17, A19, A50, FUNCT_1:def 8;
then A52: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A50, PARTFUN1:def 8;

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 A53: g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ; :: thesis: contradiction

A54: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A50, A51, PARTFUN1:def 8;
((Index ((NW-corner (L~ f)),g)) + 1) + 1 <> len g by A2, A18, A53, XBOOLE_0:3;
then ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A46, XXREAL_0:1;
then A55: (((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 A48, TOPREAL1:27;
then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A3, A6, A10, A46, A48, A47, A53, A55, A54, JORDAN5C:28;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

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

A57: now

assume A58: 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 A59: 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 A58;
A60: ( 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:41;
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 A10, A46, TOPREAL1:def 5;
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 A47, A60, SPPOL_1:63, SPPOL_1:64;
hence contradiction by A59, EUCLID:56; :: 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, A46, A48, A49, JORDAN3:39;
A61: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A2, A46, A57, XXREAL_0:1;
g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in (L~ f) ` by A56, SUBSET_1:50;
then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:11;
then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in LeftComp f by A57, XBOOLE_0:def 3;
then A62: m /. 1 in LeftComp f by A8, A50, SPRECT_2:12;
m /. (len m) in RightComp f by A2, A8, A50, SPRECT_2:13;
then L~ f meets L~ m by A62, Th50;
then consider q being set such that
A63: q in L~ f and
A64: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A64;
consider i being Element of NAT such that
A65: 1 <= i and
A66: i + 1 <= len m and
A67: q in LSeg (m,i) by A64, SPPOL_2:13;
set j = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1;
A68: len m = ((len g) -' (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) + 1 by A46, A48, JORDAN4:20;
then len m = (len g) -' ((Index ((NW-corner (L~ f)),g)) + 1) by A45, NAT_2:9;
then (len m) + ((Index ((NW-corner (L~ f)),g)) + 1) = len g by A16, XREAL_1:237;
then (i + 1) + ((Index ((NW-corner (L~ f)),g)) + 1) <= len g by A66, XREAL_1:8;
then A69: ((i + 1) + (Index ((NW-corner (L~ f)),g))) + 1 <= len g ;
i < len m by A66, NAT_1:13;
then A70: LSeg (m,i) = LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1)) by A48, A61, A65, A68, JORDAN4:31;
A71: (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 A72: (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A65, XREAL_1:8;

A73: now

assume NW-corner (L~ f) = q ; :: thesis: contradiction
then A74: 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 A47, A67, A70, XBOOLE_0:def 4;
then A75: 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 A72, XXREAL_0:1;

suppose A76: ((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 A61, 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 A10, TOPREAL1:def 8;
hence contradiction by A52, A74, A76, 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 A75, TOPREAL1:def 9; :: thesis: verum

end;

end;

end;

0 + 1 <= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A71, NAT_1:11;
then (Index ((NW-corner (L~ f)),g)) + 1 >= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A3, A6, A10, A46, A47, A63, A67, A70, A71, A69, A73, JORDAN5C:28;
then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A72, XXREAL_0:2;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

end;