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, Th50;
A5: (L~ f) /\ (L~ g) is closed by TOPS_1:35;
assume A6: 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;
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 (SE-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: SE-corner (L~ f) in (L~ g) /\ (L~ f) by A3, A5, A6, JORDAN5C:def 2;
then A12: SE-corner (L~ f) in L~ g by XBOOLE_0:def 4;
then A13: 1 <= Index (SE-corner (L~ f)),g by JORDAN3:41;
A14: SE-corner (L~ f) in LSeg g,(Index (SE-corner (L~ f)),g) by A12, JORDAN3:42;
A15: Index (SE-corner (L~ f)),g < len g by A12, JORDAN3:41;
then A16: (Index (SE-corner (L~ f)),g) + 1 <= len g by NAT_1:13;
then A17: (Index (SE-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 SE-corner (L~ f) <> g . ((Index (SE-corner (L~ f)),g) + 1) ; :: thesis: contradiction
then A21: SE-corner (L~ f) <> g /. ((Index (SE-corner (L~ f)),g) + 1) by A17, PARTFUN1:def 8;
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 A24: not g /. ((Index (SE-corner (L~ f)),g) + 1) in L~ f ; :: thesis: contradiction
A25: now
assume A26: 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 Th54;
then A27: 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 A26;
A28: ( LSeg g,(Index (SE-corner (L~ f)),g) is vertical or LSeg g,(Index (SE-corner (L~ f)),g) is horizontal ) by SPPOL_1:41;
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 A13, A16, TOPREAL1:def 5;
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 A14, A28, SPPOL_1:63, SPPOL_1:64;
hence contradiction by A27, EUCLID:56; :: thesis: verum
end;
then reconsider m = mid g,((Index (SE-corner (L~ f)),g) + 1),(len g) as S-Sequence_in_R2 by A2, A16, A10, A20, JORDAN3:39;
A29: (Index (SE-corner (L~ f)),g) + 1 < len g by A2, A16, A25, XXREAL_0:1;
g /. ((Index (SE-corner (L~ f)),g) + 1) in (L~ f) ` by A24, SUBSET_1:50;
then g /. ((Index (SE-corner (L~ f)),g) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:11;
then g /. ((Index (SE-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 (SE-corner (L~ f)),g) + 1)) -' 1;
A36: (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 ;
A37: len m = ((len g) -' ((Index (SE-corner (L~ f)),g) + 1)) + 1 by A16, A10, JORDAN4:20;
then len m = (len g) -' (Index (SE-corner (L~ f)),g) by A12, JORDAN3:41, NAT_2:9;
then (len m) + (Index (SE-corner (L~ f)),g) = len g by A15, XREAL_1:237;
then (i + 1) + (Index (SE-corner (L~ f)),g) <= len g by A34, XREAL_1:8;
then A38: ((i + ((Index (SE-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 (SE-corner (L~ f)),g) + 1)) -' 1) by A10, A29, A33, A37, JORDAN4:31;
A40: (i + ((Index (SE-corner (L~ f)),g) + 1)) -' 1 >= (Index (SE-corner (L~ f)),g) + 1 by A33, A36, XREAL_1:8;
A41: now
assume SE-corner (L~ f) = q ; :: thesis: contradiction
then A42: 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 A14, A35, A39, XBOOLE_0:def 4;
then A43: LSeg g,(Index (SE-corner (L~ f)),g) meets LSeg g,((i + ((Index (SE-corner (L~ f)),g) + 1)) -' 1) by XBOOLE_0:4;
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 A40, XXREAL_0:1;
suppose A44: (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 A29, 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 A13, TOPREAL1:def 8;
hence contradiction by A21, A42, A44, 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 A43, TOPREAL1:def 9; :: thesis: verum
end;
end;
end;
Index (SE-corner (L~ f)),g >= 0 by NAT_1:2;
then 0 + 1 <= (i + ((Index (SE-corner (L~ f)),g) + 1)) -' 1 by A33, A36, XREAL_1:9;
then Index (SE-corner (L~ f)),g >= (i + ((Index (SE-corner (L~ f)),g) + 1)) -' 1 by A3, A6, A13, A16, A14, A31, A35, A39, A38, A41, JORDAN5C:28;
then Index (SE-corner (L~ f)),g >= (Index (SE-corner (L~ f)),g) + 1 by A40, XXREAL_0:2;
hence contradiction by XREAL_1:31; :: thesis: verum
end;
end;
end;
SE-corner (L~ f) in L~ f by A11, XBOOLE_0:def 4;
then SE-corner (L~ f) <> g . (len g) by A2, A18, A9, XBOOLE_0:3;
then A45: (Index (SE-corner (L~ f)),g) + 1 < len g by A16, A19, XXREAL_0:1;
then A46: ((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 A10, TOPREAL1:27;
then A47: SE-corner (L~ f) in LSeg g,((Index (SE-corner (L~ f)),g) + 1) by A17, A19, PARTFUN1:def 8;
A48: 1 <= ((Index (SE-corner (L~ f)),g) + 1) + 1 by NAT_1:11;
then A49: len g >= 1 by A46, XXREAL_0:2;
A50: ((Index (SE-corner (L~ f)),g) + 1) + 1 in dom g by A46, A48, FINSEQ_3:27;
(Index (SE-corner (L~ f)),g) + 1 < ((Index (SE-corner (L~ f)),g) + 1) + 1 by NAT_1:13;
then A51: SE-corner (L~ f) <> g . (((Index (SE-corner (L~ f)),g) + 1) + 1) by A17, A19, A50, FUNCT_1:def 8;
then A52: SE-corner (L~ f) <> g /. (((Index (SE-corner (L~ f)),g) + 1) + 1) by A50, PARTFUN1:def 8;
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 A53: g /. (((Index (SE-corner (L~ f)),g) + 1) + 1) in L~ f ; :: thesis: contradiction
A54: SE-corner (L~ f) <> g /. (((Index (SE-corner (L~ f)),g) + 1) + 1) by A50, A51, PARTFUN1:def 8;
((Index (SE-corner (L~ f)),g) + 1) + 1 <> len g by A2, A18, A53, XBOOLE_0:3;
then ((Index (SE-corner (L~ f)),g) + 1) + 1 < len g by A46, XXREAL_0:1;
then A55: (((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 A48, TOPREAL1:27;
then (Index (SE-corner (L~ f)),g) + 1 >= ((Index (SE-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 (SE-corner (L~ f)),g) + 1) + 1) in L~ f ; :: thesis: contradiction
A57: now
assume A58: 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 Th54;
then A59: 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 A58;
A60: ( 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:41;
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 A10, A46, TOPREAL1:def 5;
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 A47, A60, SPPOL_1:63, SPPOL_1:64;
hence contradiction by A59, EUCLID:56; :: 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, A46, A48, A49, JORDAN3:39;
A61: ((Index (SE-corner (L~ f)),g) + 1) + 1 < len g by A2, A46, A57, XXREAL_0:1;
g /. (((Index (SE-corner (L~ f)),g) + 1) + 1) in (L~ f) ` by A56, SUBSET_1:50;
then g /. (((Index (SE-corner (L~ f)),g) + 1) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:11;
then g /. (((Index (SE-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 (SE-corner (L~ f)),g) + 1) + 1)) -' 1;
A68: len m = ((len g) -' (((Index (SE-corner (L~ f)),g) + 1) + 1)) + 1 by A46, A48, JORDAN4:20;
then len m = (len g) -' ((Index (SE-corner (L~ f)),g) + 1) by A45, NAT_2:9;
then (len m) + ((Index (SE-corner (L~ f)),g) + 1) = len g by A16, XREAL_1:237;
then (i + 1) + ((Index (SE-corner (L~ f)),g) + 1) <= len g by A66, XREAL_1:8;
then A69: ((i + 1) + (Index (SE-corner (L~ f)),g)) + 1 <= len g ;
i < len m by A66, NAT_1:13;
then A70: LSeg m,i = LSeg g,((i + (((Index (SE-corner (L~ f)),g) + 1) + 1)) -' 1) by A48, A61, A65, A68, JORDAN4:31;
A71: (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 A72: (i + (((Index (SE-corner (L~ f)),g) + 1) + 1)) -' 1 >= ((Index (SE-corner (L~ f)),g) + 1) + 1 by A65, XREAL_1:8;
A73: now
assume SE-corner (L~ f) = q ; :: thesis: contradiction
then A74: 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 A47, A67, A70, XBOOLE_0:def 4;
then A75: LSeg g,((Index (SE-corner (L~ f)),g) + 1) meets LSeg g,((i + (((Index (SE-corner (L~ f)),g) + 1) + 1)) -' 1) by XBOOLE_0:4;
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 A72, XXREAL_0:1;
suppose A76: ((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 A61, 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 A10, TOPREAL1:def 8;
hence contradiction by A52, A74, A76, 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 A75, TOPREAL1:def 9; :: thesis: verum
end;
end;
end;
0 + 1 <= (i + (((Index (SE-corner (L~ f)),g) + 1) + 1)) -' 1 by A71, NAT_1:11;
then (Index (SE-corner (L~ f)),g) + 1 >= (i + (((Index (SE-corner (L~ f)),g) + 1) + 1)) -' 1 by A3, A6, A10, A46, A47, A63, A67, A70, A71, A69, A73, JORDAN5C:28;
then (Index (SE-corner (L~ f)),g) + 1 >= ((Index (SE-corner (L~ f)),g) + 1) + 1 by A72, XXREAL_0:2;
hence contradiction by XREAL_1:31; :: thesis: verum
end;
end;