let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )
set x = N-max (L~ (Cage (C,n)));
set p = W-min (L~ (Cage (C,n)));
set f = Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))));
A1:
rng (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = rng (Cage (C,n))
by FINSEQ_6:90, SPRECT_2:46;
A2:
N-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:40;
A3:
(Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n)))
by JORDAN1F:6;
A4:
L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by REVROT_1:33;
W-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:43;
then A5:
W-min (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by FINSEQ_6:90, SPRECT_2:46;
A6:
W-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:43;
Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))
by JORDAN1G:18;
then A7:
(Lower_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. 1
by A5, FINSEQ_5:44;
then A8:
(W-min (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) < (W-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by A4, JORDAN1F:6, SPRECT_5:42;
A9:
(W-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) <= (N-min (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by A7, A4, JORDAN1F:6, SPRECT_5:43;
per cases
( N-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))) <> E-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))) or N-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))) = E-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))) )
;
suppose
N-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))) <> E-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))
;
( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )then
(W-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) < (N-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by A7, A3, A4, A9, SPRECT_5:44, XXREAL_0:2;
then
N-max (L~ (Cage (C,n))) in rng ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) :- (W-min (L~ (Cage (C,n)))))
by A1, A2, A6, A4, A8, FINSEQ_6:62, XXREAL_0:2;
hence A10:
N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by Th4;
N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n))
len (Upper_Seq (C,n)) >= 2
by TOPREAL1:def 8;
then
rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n))
by SPPOL_2:18;
hence
N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n))
by A10;
verum end; suppose A11:
N-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))) = E-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))
;
( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )A12:
(E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:46;
then A13:
E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by FINSEQ_6:90, SPRECT_2:43;
Upper_Seq (
C,
n)
= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))
by JORDAN1E:def 1;
hence A14:
N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by A4, A11, A13, A12, FINSEQ_5:46;
N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n))
len (Upper_Seq (C,n)) >= 2
by TOPREAL1:def 8;
then
rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n))
by SPPOL_2:18;
hence
N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n))
by A14;
verum end; end;