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;
A4: L~ f is closed by SPPOL_1:49;
( L~ f is closed & L~ g is closed ) by SPPOL_1:49;
then A5: (L~ f) /\ (L~ g) is closed by TOPS_1:35;
A6: L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:31;
set nw = NW-corner (L~ f);
set inw = Index (NW-corner (L~ f)),g;
assume A7: Last_Point (L~ g),(g /. 1),(g /. (len g)),(L~ f) = NW-corner (L~ f) ; :: thesis: contradiction
then A8: NW-corner (L~ f) in (L~ g) /\ (L~ f) by A3, A5, A6, JORDAN5C:def 2;
then A9: NW-corner (L~ f) in L~ g by XBOOLE_0:def 4;
A10: L~ f misses RightComp f by Th42;
A11: NW-corner (L~ f) in L~ f by A8, XBOOLE_0:def 4;
A12: len g in dom g by FINSEQ_5:6;
then g . (len g) = g /. (len g) by PARTFUN1:def 8;
then A13: NW-corner (L~ f) <> g . (len g) by A2, A10, A11, XBOOLE_0:3;
A14: Index (NW-corner (L~ f)),g < len g by A9, JORDAN3:41;
then A15: ( 1 <= Index (NW-corner (L~ f)),g & (Index (NW-corner (L~ f)),g) + 1 <= len g ) by A9, JORDAN3:41, NAT_1:13;
A16: NW-corner (L~ f) in LSeg g,(Index (NW-corner (L~ f)),g) by A9, JORDAN3:42;
A17: 1 <= (Index (NW-corner (L~ f)),g) + 1 by NAT_1:11;
then A18: (Index (NW-corner (L~ f)),g) + 1 in dom g by A15, FINSEQ_3:27;

A19: now

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

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, A10, XBOOLE_0:3;
then (Index (NW-corner (L~ f)),g) + 1 < len g by A15, 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 A17, TOPREAL1:27;
then Index (NW-corner (L~ f)),g >= (Index (NW-corner (L~ f)),g) + 1 by A3, A4, A7, A15, A16, A17, A20, A22, A23, JORDAN5C:28;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

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

then g /. ((Index (NW-corner (L~ f)),g) + 1) in (L~ f) ` by SUBSET_1:50;
then A24: g /. ((Index (NW-corner (L~ f)),g) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:11;

A25: now

A26: 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;
assume g /. ((Index (NW-corner (L~ f)),g) + 1) in RightComp f ; :: thesis: contradiction
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) = LSeg (g /. (Index (NW-corner (L~ f)),g)),(g /. ((Index (NW-corner (L~ f)),g) + 1)) by A15, TOPREAL1:def 5;
( 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;
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 A16, A28, SPPOL_1:63, SPPOL_1:64;
hence contradiction by A27, EUCLID:56; :: thesis: verum

end;

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

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 A16, A35, A37, 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 A41, 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 A30, 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 A15, TOPREAL1:def 8;
hence contradiction by A20, 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;

then Index (NW-corner (L~ f)),g >= (i + ((Index (NW-corner (L~ f)),g) + 1)) -' 1 by A3, A4, A7, A15, A16, A32, A35, A37, A39, A40, JORDAN5C:28;
then Index (NW-corner (L~ f)),g >= (Index (NW-corner (L~ f)),g) + 1 by A41, XXREAL_0:2;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

end;

end;

then A45: (Index (NW-corner (L~ f)),g) + 1 < len g by A13, A15, XXREAL_0:1;
then A46: ((Index (NW-corner (L~ f)),g) + 1) + 1 <= len g by NAT_1:13;
A47: 1 <= ((Index (NW-corner (L~ f)),g) + 1) + 1 by NAT_1:11;
then A48: ((Index (NW-corner (L~ f)),g) + 1) + 1 in dom g by A46, FINSEQ_3:27;
g /. ((Index (NW-corner (L~ f)),g) + 1) in LSeg g,((Index (NW-corner (L~ f)),g) + 1) by A17, A46, TOPREAL1:27;
then A49: NW-corner (L~ f) in LSeg g,((Index (NW-corner (L~ f)),g) + 1) by A18, A19, PARTFUN1:def 8;
(Index (NW-corner (L~ f)),g) + 1 < ((Index (NW-corner (L~ f)),g) + 1) + 1 by NAT_1:13;
then A50: NW-corner (L~ f) <> g . (((Index (NW-corner (L~ f)),g) + 1) + 1) by A18, A19, A48, FUNCT_1:def 8;
then A51: NW-corner (L~ f) <> g /. (((Index (NW-corner (L~ f)),g) + 1) + 1) by A48, PARTFUN1:def 8;
A52: len g >= 1 by A46, A47, XXREAL_0:2;

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

then ((Index (NW-corner (L~ f)),g) + 1) + 1 <> len g by A2, A10, XBOOLE_0:3;
then ((Index (NW-corner (L~ f)),g) + 1) + 1 < len g by A46, XXREAL_0:1;
then A54: (((Index (NW-corner (L~ f)),g) + 1) + 1) + 1 <= len g by NAT_1:13;
then A55: g /. (((Index (NW-corner (L~ f)),g) + 1) + 1) in LSeg g,(((Index (NW-corner (L~ f)),g) + 1) + 1) by A47, TOPREAL1:27;
NW-corner (L~ f) <> g /. (((Index (NW-corner (L~ f)),g) + 1) + 1) by A48, A50, PARTFUN1:def 8;
then (Index (NW-corner (L~ f)),g) + 1 >= ((Index (NW-corner (L~ f)),g) + 1) + 1 by A3, A4, A7, A17, A46, A47, A49, A53, A54, A55, JORDAN5C:28;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

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

then g /. (((Index (NW-corner (L~ f)),g) + 1) + 1) in (L~ f) ` by SUBSET_1:50;
then A56: g /. (((Index (NW-corner (L~ f)),g) + 1) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:11;

A57: now

A58: 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;
assume g /. (((Index (NW-corner (L~ f)),g) + 1) + 1) in RightComp f ; :: thesis: contradiction
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) = LSeg (g /. ((Index (NW-corner (L~ f)),g) + 1)),(g /. (((Index (NW-corner (L~ f)),g) + 1) + 1)) by A17, A46, TOPREAL1:def 5;
( 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;
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 A49, A60, SPPOL_1:63, SPPOL_1:64;
hence contradiction by A59, EUCLID:56; :: thesis: verum

end;

then A61: g /. (((Index (NW-corner (L~ f)),g) + 1) + 1) in LeftComp f by A56, XBOOLE_0:def 3;
A62: ((Index (NW-corner (L~ f)),g) + 1) + 1 < len g by A2, A46, A57, XXREAL_0:1;
reconsider m = mid g,(((Index (NW-corner (L~ f)),g) + 1) + 1),(len g) as S-Sequence_in_R2 by A2, A46, A47, A52, A57, JORDAN3:39;
A63: m /. 1 in LeftComp f by A12, A48, A61, SPRECT_2:12;
m /. (len m) in RightComp f by A2, A12, A48, SPRECT_2:13;
then L~ f meets L~ m by A63, Th50;
then consider q being set such that
A64: q in L~ f and
A65: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A65;
consider i being Element of NAT such that
A66: ( 1 <= i & i + 1 <= len m ) and
A67: q in LSeg m,i by A65, SPPOL_2:13;
A68: len m = ((len g) -' (((Index (NW-corner (L~ f)),g) + 1) + 1)) + 1 by A46, A47, JORDAN4:20;
i < len m by A66, NAT_1:13;
then A69: LSeg m,i = LSeg g,((i + (((Index (NW-corner (L~ f)),g) + 1) + 1)) -' 1) by A47, A62, A66, A68, JORDAN4:31;
set j = (i + (((Index (NW-corner (L~ f)),g) + 1) + 1)) -' 1;
A70: (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 A71: 0 + 1 <= (i + (((Index (NW-corner (L~ f)),g) + 1) + 1)) -' 1 by NAT_1:11;
len m = (len g) -' ((Index (NW-corner (L~ f)),g) + 1) by A45, A68, NAT_2:9;
then (len m) + ((Index (NW-corner (L~ f)),g) + 1) = len g by A15, XREAL_1:237;
then (i + 1) + ((Index (NW-corner (L~ f)),g) + 1) <= len g by A66, XREAL_1:8;
then A72: ((i + 1) + (Index (NW-corner (L~ f)),g)) + 1 <= len g ;
(i + (((Index (NW-corner (L~ f)),g) + 1) + 1)) -' 1 = i + ((Index (NW-corner (L~ f)),g) + 1) by A70;
then A73: (i + (((Index (NW-corner (L~ f)),g) + 1) + 1)) -' 1 >= ((Index (NW-corner (L~ f)),g) + 1) + 1 by A66, XREAL_1:8;

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 A49, A67, A69, 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 A73, 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 A62, 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 A17, TOPREAL1:def 8;
hence contradiction by A51, 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;

then (Index (NW-corner (L~ f)),g) + 1 >= (i + (((Index (NW-corner (L~ f)),g) + 1) + 1)) -' 1 by A3, A4, A7, A17, A46, A49, A64, A67, A69, A70, A71, A72, JORDAN5C:28;
then (Index (NW-corner (L~ f)),g) + 1 >= ((Index (NW-corner (L~ f)),g) + 1) + 1 by A73, XXREAL_0:2;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

end;