let f be rectangular special_circular_sequence; 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; ( 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
; 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;
assume A5:
Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = SE-corner (L~ f)
; contradiction
set se = SE-corner (L~ f);
set ise = Index ((SE-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 ((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 A9:
SE-corner (L~ f) in (L~ g) /\ (L~ f)
by A3, A5, JORDAN5C:def 2;
then A10:
SE-corner (L~ f) in L~ g
by XBOOLE_0:def 4;
then A11:
1 <= Index ((SE-corner (L~ f)),g)
by JORDAN3:8;
A12:
SE-corner (L~ f) in LSeg (g,(Index ((SE-corner (L~ f)),g)))
by A10, JORDAN3:9;
A13:
Index ((SE-corner (L~ f)),g) < len g
by A10, JORDAN3:8;
then A14:
(Index ((SE-corner (L~ f)),g)) + 1 <= len g
by NAT_1:13;
then A15:
(Index ((SE-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
SE-corner (L~ f) <> g . ((Index ((SE-corner (L~ f)),g)) + 1)
;
contradictionthen A19:
SE-corner (L~ f) <> g /. ((Index ((SE-corner (L~ f)),g)) + 1)
by A15, 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 A20:
g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f
;
contradictionthen
(Index ((SE-corner (L~ f)),g)) + 1
<> len g
by A2, A16, XBOOLE_0:3;
then
(Index ((SE-corner (L~ f)),g)) + 1
< len g
by A14, XXREAL_0:1;
then A21:
((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 A8, TOPREAL1:21;
then
Index (
(SE-corner (L~ f)),
g)
>= (Index ((SE-corner (L~ f)),g)) + 1
by A3, A5, A11, A14, A12, A8, A19, A20, A21, JORDAN5C:28;
hence
contradiction
by XREAL_1:29;
verum end; suppose A22:
not
g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f
;
contradictionA23:
now assume A24:
g /. ((Index ((SE-corner (L~ f)),g)) + 1) in RightComp f
;
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 ((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 A24;
A26:
(
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 A11, A14, 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 A12, A26, SPPOL_1:40, SPPOL_1:41;
hence
contradiction
by A25, EUCLID:52;
verum end; then reconsider m =
mid (
g,
((Index ((SE-corner (L~ f)),g)) + 1),
(len g)) as
S-Sequence_in_R2 by A2, A14, A8, A18, JORDAN3:6;
A27:
(Index ((SE-corner (L~ f)),g)) + 1
< len g
by A2, A14, A23, XXREAL_0:1;
g /. ((Index ((SE-corner (L~ f)),g)) + 1) in (L~ f) `
by A22, 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 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 ((SE-corner (L~ f)),g)) + 1)) -' 1;
A34:
(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
;
A35:
len m = ((len g) -' ((Index ((SE-corner (L~ f)),g)) + 1)) + 1
by A14, A8, JORDAN4:8;
then
len m = (len g) -' (Index ((SE-corner (L~ f)),g))
by A10, JORDAN3:8, NAT_2:7;
then
(len m) + (Index ((SE-corner (L~ f)),g)) = len g
by A13, XREAL_1:235;
then
(i + 1) + (Index ((SE-corner (L~ f)),g)) <= len g
by A32, XREAL_1:6;
then A36:
((i + ((Index ((SE-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 ((SE-corner (L~ f)),g)) + 1)) -' 1))
by A8, A27, A31, A35, JORDAN4:19;
A38:
(i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1
>= (Index ((SE-corner (L~ f)),g)) + 1
by A31, A34, XREAL_1:6;
A39:
now assume
SE-corner (L~ f) = q
;
contradictionthen A40:
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 A12, A33, A37, XBOOLE_0:def 4;
then A41:
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 A38, XXREAL_0:1;
suppose A42:
(Index ((SE-corner (L~ f)),g)) + 1
= (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1
;
contradiction
((Index ((SE-corner (L~ f)),g)) + 1) + 1
<= len g
by A27, 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 A11, TOPREAL1:def 6;
hence
contradiction
by A19, A40, A42, TARSKI:def 1;
verum 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 A31, A34, XREAL_1:7;
then
Index (
(SE-corner (L~ f)),
g)
>= (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1
by A3, A5, A11, A14, A12, A29, A33, A37, A36, A39, JORDAN5C:28;
then
Index (
(SE-corner (L~ f)),
g)
>= (Index ((SE-corner (L~ f)),g)) + 1
by A38, XXREAL_0:2;
hence
contradiction
by XREAL_1:29;
verum end;
SE-corner (L~ f) in L~ f
by A9, XBOOLE_0:def 4;
then
SE-corner (L~ f) <> g . (len g)
by A2, A16, A7, XBOOLE_0:3;
then A43:
(Index ((SE-corner (L~ f)),g)) + 1 < len g
by A14, A17, XXREAL_0:1;
then A44:
((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 A8, TOPREAL1:21;
then A45:
SE-corner (L~ f) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))
by A15, A17, PARTFUN1:def 6;
A46:
1 <= ((Index ((SE-corner (L~ f)),g)) + 1) + 1
by NAT_1:11;
then A47:
len g >= 1
by A44, XXREAL_0:2;
A48:
((Index ((SE-corner (L~ f)),g)) + 1) + 1 in dom g
by A44, A46, FINSEQ_3:25;
(Index ((SE-corner (L~ f)),g)) + 1 < ((Index ((SE-corner (L~ f)),g)) + 1) + 1
by NAT_1:13;
then A49:
SE-corner (L~ f) <> g . (((Index ((SE-corner (L~ f)),g)) + 1) + 1)
by A15, A17, A48, FUNCT_1:def 4;
then A50:
SE-corner (L~ f) <> g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1)
by A48, 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 A51:
g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f
;
contradictionA52:
SE-corner (L~ f) <> g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1)
by A48, A49, PARTFUN1:def 6;
((Index ((SE-corner (L~ f)),g)) + 1) + 1
<> len g
by A2, A16, A51, XBOOLE_0:3;
then
((Index ((SE-corner (L~ f)),g)) + 1) + 1
< len g
by A44, XXREAL_0:1;
then A53:
(((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 A46, TOPREAL1:21;
then
(Index ((SE-corner (L~ f)),g)) + 1
>= ((Index ((SE-corner (L~ f)),g)) + 1) + 1
by A3, A5, A8, A44, A46, A45, A51, A53, A52, JORDAN5C:28;
hence
contradiction
by XREAL_1:29;
verum end; suppose A54:
not
g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f
;
contradictionA55:
now assume A56:
g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in RightComp f
;
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 ((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 A56;
A58:
(
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 A8, A44, 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 A45, A58, SPPOL_1:40, SPPOL_1:41;
hence
contradiction
by A57, EUCLID:52;
verum end; then reconsider m =
mid (
g,
(((Index ((SE-corner (L~ f)),g)) + 1) + 1),
(len g)) as
S-Sequence_in_R2 by A2, A44, A46, A47, JORDAN3:6;
A59:
((Index ((SE-corner (L~ f)),g)) + 1) + 1
< len g
by A2, A44, A55, XXREAL_0:1;
g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in (L~ f) `
by A54, 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 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 ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1;
A66:
len m = ((len g) -' (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) + 1
by A44, A46, JORDAN4:8;
then
len m = (len g) -' ((Index ((SE-corner (L~ f)),g)) + 1)
by A43, NAT_2:7;
then
(len m) + ((Index ((SE-corner (L~ f)),g)) + 1) = len g
by A14, XREAL_1:235;
then
(i + 1) + ((Index ((SE-corner (L~ f)),g)) + 1) <= len g
by A64, XREAL_1:6;
then A67:
((i + 1) + (Index ((SE-corner (L~ f)),g))) + 1
<= len g
;
i < len m
by A64, NAT_1:13;
then A68:
LSeg (
m,
i)
= LSeg (
g,
((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1))
by A46, A59, A63, A66, JORDAN4:19;
A69:
(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 A70:
(i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1
>= ((Index ((SE-corner (L~ f)),g)) + 1) + 1
by A63, XREAL_1:6;
A71:
now assume
SE-corner (L~ f) = q
;
contradictionthen A72:
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 A45, A65, A68, XBOOLE_0:def 4;
then A73:
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 A70, XXREAL_0:1;
suppose A74:
((Index ((SE-corner (L~ f)),g)) + 1) + 1
= (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1
;
contradiction
(((Index ((SE-corner (L~ f)),g)) + 1) + 1) + 1
<= len g
by A59, 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 A8, TOPREAL1:def 6;
hence
contradiction
by A50, A72, A74, TARSKI:def 1;
verum end; end;
0 + 1
<= (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1
by A69, NAT_1:11;
then
(Index ((SE-corner (L~ f)),g)) + 1
>= (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1
by A3, A5, A8, A44, A45, A61, A65, A68, A69, A67, A71, JORDAN5C:28;
then
(Index ((SE-corner (L~ f)),g)) + 1
>= ((Index ((SE-corner (L~ f)),g)) + 1) + 1
by A70, XXREAL_0:2;
hence
contradiction
by XREAL_1:29;
verum