let n be Nat; for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) < (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) < (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
set Wmi = W-min (L~ (Cage (C,n)));
set Nmi = N-min (L~ (Cage (C,n)));
set Nma = N-max (L~ (Cage (C,n)));
set Ema = E-max (L~ (Cage (C,n)));
set Rot = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
A1:
L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = L~ (Cage (C,n))
by REVROT_1:33;
then A2:
E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by SPRECT_2:46;
W-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:43;
then
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Cage (C,n)))
by FINSEQ_6:92;
then A3:
( (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < (N-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) & (N-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)))))) )
by A1, SPRECT_5:24, SPRECT_5:25;
A4:
N-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by A1, SPRECT_2:40;
N-min (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by A1, SPRECT_2:39;
then
( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & (N-min (L~ (Cage (C,n)))) .. ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) = (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) )
by A2, A3, JORDAN1E:def 1, SPRECT_5:3, XXREAL_0:2;
hence
(N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) < (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
by A2, A3, A4, SPRECT_5:3; verum