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)) <> SE-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)) <> SE-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)) <> SE-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)) = SE-corner (L~ f) ; :: thesis: contradiction
set se = SE-corner (L~ f);
set ise = Index ((SE-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 ((SE-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: SE-corner (L~ f) in (L~ g) /\ (L~ f) by A3, A4, JORDAN5C:def 2;
then A9: SE-corner (L~ f) in L~ g by XBOOLE_0:def 4;
then A10: 1 <= Index ((SE-corner (L~ f)),g) by JORDAN3:8;
A11: SE-corner (L~ f) in LSeg (g,(Index ((SE-corner (L~ f)),g))) by A9, JORDAN3:9;
A12: Index ((SE-corner (L~ f)),g) < len g by A9, JORDAN3:8;
then A13: (Index ((SE-corner (L~ f)),g)) + 1 <= len g by NAT_1:13;
then A14: (Index ((SE-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 SE-corner (L~ f) <> g . ((Index ((SE-corner (L~ f)),g)) + 1)

A17: len g >= 1 by A13, A7, XXREAL_0:2;
assume SE-corner (L~ f) <> g . ((Index ((SE-corner (L~ f)),g)) + 1) ; :: thesis: contradiction
then A18: SE-corner (L~ f) <> g /. ((Index ((SE-corner (L~ f)),g)) + 1) by A14, PARTFUN1:def 6;

per cases ( g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f or not g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f ) ;

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

then (Index ((SE-corner (L~ f)),g)) + 1 <> len g by A2, A15, XBOOLE_0:3;
then (Index ((SE-corner (L~ f)),g)) + 1 < len g by A13, XXREAL_0:1;
then A20: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13;
then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21;
then Index ((SE-corner (L~ f)),g) >= (Index ((SE-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 ((SE-corner (L~ f)),g)) + 1) in L~ f ; :: thesis: contradiction

A22: now :: thesis: not g /. ((Index ((SE-corner (L~ f)),g)) + 1) in RightComp f

assume A23: g /. ((Index ((SE-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 ((SE-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 ((SE-corner (L~ f)),g))) is vertical or LSeg (g,(Index ((SE-corner (L~ f)),g))) is horizontal ) by SPPOL_1:19;
LSeg (g,(Index ((SE-corner (L~ f)),g))) = LSeg ((g /. (Index ((SE-corner (L~ f)),g))),(g /. ((Index ((SE-corner (L~ f)),g)) + 1))) by A10, A13, TOPREAL1:def 3;
then ( (g /. ((Index ((SE-corner (L~ f)),g)) + 1)) `1 = (SE-corner (L~ f)) `1 or (g /. ((Index ((SE-corner (L~ f)),g)) + 1)) `2 = (SE-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 ((SE-corner (L~ f)),g)) + 1),(len g)) as S-Sequence_in_R2 by A2, A13, A7, A17, JORDAN3:6;
A26: (Index ((SE-corner (L~ f)),g)) + 1 < len g by A2, A13, A22, XXREAL_0:1;
g /. ((Index ((SE-corner (L~ f)),g)) + 1) in (L~ f) ` by A21, SUBSET_1:29;
then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then g /. ((Index ((SE-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 ((SE-corner (L~ f)),g)) + 1)) -' 1;
A33: (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 = ((i + (Index ((SE-corner (L~ f)),g))) + 1) -' 1
.= i + (Index ((SE-corner (L~ f)),g)) by NAT_D:34 ;
A34: len m = ((len g) -' ((Index ((SE-corner (L~ f)),g)) + 1)) + 1 by A13, A7, FINSEQ_6:186;
then len m = (len g) -' (Index ((SE-corner (L~ f)),g)) by A9, JORDAN3:8, NAT_2:7;
then (len m) + (Index ((SE-corner (L~ f)),g)) = len g by A12, XREAL_1:235;
then (i + 1) + (Index ((SE-corner (L~ f)),g)) <= len g by A31, XREAL_1:6;
then A35: ((i + ((Index ((SE-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 ((SE-corner (L~ f)),g)) + 1)) -' 1)) by A7, A26, A30, A34, JORDAN4:19;
A37: (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 >= (Index ((SE-corner (L~ f)),g)) + 1 by A30, A33, XREAL_1:6;

A38: now :: thesis: not SE-corner (L~ f) = q

assume SE-corner (L~ f) = q ; :: thesis: contradiction
then A39: SE-corner (L~ f) in (LSeg (g,(Index ((SE-corner (L~ f)),g)))) /\ (LSeg (g,((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1))) by A11, A32, A36, XBOOLE_0:def 4;
then A40: LSeg (g,(Index ((SE-corner (L~ f)),g))) meets LSeg (g,((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1)) ;

per cases ( (Index ((SE-corner (L~ f)),g)) + 1 = (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 or (Index ((SE-corner (L~ f)),g)) + 1 < (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 ) by A37, XXREAL_0:1;

suppose A41: (Index ((SE-corner (L~ f)),g)) + 1 = (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 ; :: thesis: contradiction

((Index ((SE-corner (L~ f)),g)) + 1) + 1 <= len g by A26, NAT_1:13;
then (Index ((SE-corner (L~ f)),g)) + (1 + 1) <= len g ;
then (LSeg (g,(Index ((SE-corner (L~ f)),g)))) /\ (LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))) = {(g /. ((Index ((SE-corner (L~ f)),g)) + 1))} by A10, TOPREAL1:def 6;
hence contradiction by A18, A39, A41, TARSKI:def 1; :: thesis: verum

end;

suppose (Index ((SE-corner (L~ f)),g)) + 1 < (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 ; :: thesis: contradiction

hence contradiction by A40, TOPREAL1:def 7; :: thesis: verum

end;

end;

end;

0 + 1 <= (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 by A30, A33, XREAL_1:7;
then Index ((SE-corner (L~ f)),g) >= (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 by A3, A4, A10, A13, A11, A28, A32, A36, A35, A38, JORDAN5C:28;
then Index ((SE-corner (L~ f)),g) >= (Index ((SE-corner (L~ f)),g)) + 1 by A37, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

end;

end;

SE-corner (L~ f) in L~ f by A8, XBOOLE_0:def 4;
then SE-corner (L~ f) <> g . (len g) by A2, A15, A6, XBOOLE_0:3;
then A42: (Index ((SE-corner (L~ f)),g)) + 1 < len g by A13, A16, XXREAL_0:1;
then A43: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13;
then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21;
then A44: SE-corner (L~ f) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) by A14, A16, PARTFUN1:def 6;
A45: 1 <= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by NAT_1:11;
then A46: len g >= 1 by A43, XXREAL_0:2;
A47: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 in dom g by A43, A45, FINSEQ_3:25;
(Index ((SE-corner (L~ f)),g)) + 1 < ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by NAT_1:13;
then A48: SE-corner (L~ f) <> g . (((Index ((SE-corner (L~ f)),g)) + 1) + 1) by A14, A16, A47, FUNCT_1:def 4;
then A49: SE-corner (L~ f) <> g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) by A47, PARTFUN1:def 6;

per cases ( g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f or not g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f ) ;

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

A51: SE-corner (L~ f) <> g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) by A47, A48, PARTFUN1:def 6;
((Index ((SE-corner (L~ f)),g)) + 1) + 1 <> len g by A2, A15, A50, XBOOLE_0:3;
then ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < len g by A43, XXREAL_0:1;
then A52: (((Index ((SE-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by NAT_1:13;
then g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in LSeg (g,(((Index ((SE-corner (L~ f)),g)) + 1) + 1)) by A45, TOPREAL1:21;
then (Index ((SE-corner (L~ f)),g)) + 1 >= ((Index ((SE-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 ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f ; :: thesis: contradiction

A54: now :: thesis: not g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in RightComp f

assume A55: g /. (((Index ((SE-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 ((SE-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 ((SE-corner (L~ f)),g)) + 1)) is vertical or LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) is horizontal ) by SPPOL_1:19;
LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) = LSeg ((g /. ((Index ((SE-corner (L~ f)),g)) + 1)),(g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1))) by A7, A43, TOPREAL1:def 3;
then ( (g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) `1 = (SE-corner (L~ f)) `1 or (g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) `2 = (SE-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 ((SE-corner (L~ f)),g)) + 1) + 1),(len g)) as S-Sequence_in_R2 by A2, A43, A45, A46, JORDAN3:6;
A58: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < len g by A2, A43, A54, XXREAL_0:1;
g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in (L~ f) ` by A53, SUBSET_1:29;
then g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then g /. (((Index ((SE-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 ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1;
A65: len m = ((len g) -' (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) + 1 by A43, A45, FINSEQ_6:186;
then len m = (len g) -' ((Index ((SE-corner (L~ f)),g)) + 1) by A42, NAT_2:7;
then (len m) + ((Index ((SE-corner (L~ f)),g)) + 1) = len g by A13, XREAL_1:235;
then (i + 1) + ((Index ((SE-corner (L~ f)),g)) + 1) <= len g by A63, XREAL_1:6;
then A66: ((i + 1) + (Index ((SE-corner (L~ f)),g))) + 1 <= len g ;
i < len m by A63, NAT_1:13;
then A67: LSeg (m,i) = LSeg (g,((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1)) by A45, A58, A62, A65, JORDAN4:19;
A68: (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 = (((i + (Index ((SE-corner (L~ f)),g))) + 1) + 1) -' 1
.= (i + (Index ((SE-corner (L~ f)),g))) + 1 by NAT_D:34 ;
then (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 = i + ((Index ((SE-corner (L~ f)),g)) + 1) ;
then A69: (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 >= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by A62, XREAL_1:6;

A70: now :: thesis: not SE-corner (L~ f) = q

assume SE-corner (L~ f) = q ; :: thesis: contradiction
then A71: SE-corner (L~ f) in (LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))) /\ (LSeg (g,((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1))) by A44, A64, A67, XBOOLE_0:def 4;
then A72: LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) meets LSeg (g,((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1)) ;

per cases ( ((Index ((SE-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 or ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 ) by A69, XXREAL_0:1;

suppose A73: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 ; :: thesis: contradiction

(((Index ((SE-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by A58, NAT_1:13;
then ((Index ((SE-corner (L~ f)),g)) + 1) + (1 + 1) <= len g ;
then (LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))) /\ (LSeg (g,(((Index ((SE-corner (L~ f)),g)) + 1) + 1))) = {(g /. (((Index ((SE-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 ((SE-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((SE-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 ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 by A68, NAT_1:11;
then (Index ((SE-corner (L~ f)),g)) + 1 >= (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 by A3, A4, A7, A43, A44, A60, A64, A67, A68, A66, A70, JORDAN5C:28;
then (Index ((SE-corner (L~ f)),g)) + 1 >= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by A69, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

end;