let n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage C,n))) .. (Upper_Seq C,n) < (W-max (L~ (Cage C,n))) .. (Upper_Seq C,n)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: (W-min (L~ (Cage C,n))) .. (Upper_Seq C,n) < (W-max (L~ (Cage C,n))) .. (Upper_Seq C,n)
set Wmi = W-min (L~ (Cage C,n));
set Wma = W-max (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: W-min (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by SPRECT_2:47;
A3: W-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A1, SPRECT_2:48;
A4: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A1, SPRECT_2:50;
W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then A5: (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 = W-min (L~ (Cage C,n)) by FINSEQ_6:98;
then A6: (W-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) < (W-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A1, SPRECT_5:22;
A7: ( Upper_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (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, A5, JORDAN1E:def 1, SPRECT_5:26;
(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)))) by A1, A5, SPRECT_5:25;
then A8: (W-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)))) by A1, A5, SPRECT_5:24, XXREAL_0:2;
then (W-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, A5, SPRECT_5:26, XXREAL_0:2;
then (W-min (L~ (Cage C,n))) .. ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))) = (W-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A2, A4, A6, SPRECT_5:3, XXREAL_0:2;
hence (W-min (L~ (Cage C,n))) .. (Upper_Seq C,n) < (W-max (L~ (Cage C,n))) .. (Upper_Seq C,n) by A4, A6, A7, A8, A3, SPRECT_5:3, XXREAL_0:2; :: thesis: verum