let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-min (L~ (Cage C,n))) .. (Lower_Seq C,n) <= (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n)
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: (E-min (L~ (Cage C,n))) .. (Lower_Seq C,n) <= (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n)
set Ema = E-max (L~ (Cage C,n));
set Emi = E-min (L~ (Cage C,n));
set Sma = S-max (L~ (Cage C,n));
set Smi = S-min (L~ (Cage C,n));
set Wmi = W-min (L~ (Cage C,n));
set Rot = Rotate (Cage C,n),(E-max (L~ (Cage C,n)));
A1: Lower_Seq C,n = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) -: (W-min (L~ (Cage C,n))) by Th26;
A2: L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) = L~ (Cage C,n) by REVROT_1:33;
then A3: E-min (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by SPRECT_2:49;
A4: S-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A2, SPRECT_2:46;
A5: W-min (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A2, SPRECT_2:47;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A6: (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 1 = E-max (L~ (Cage C,n)) by FINSEQ_6:98;
then A7: (E-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) <= (S-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A2, SPRECT_5:40;
A8: (S-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) <= (W-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A2, A6, SPRECT_5:42;
A9: (S-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) < (S-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A2, A6, SPRECT_5:41;
then (S-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) < (W-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A2, A6, SPRECT_5:42, XXREAL_0:2;
then (E-min (L~ (Cage C,n))) .. ((Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) -: (W-min (L~ (Cage C,n)))) = (E-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A3, A5, A7, SPRECT_5:3, XXREAL_0:2;
hence (E-min (L~ (Cage C,n))) .. (Lower_Seq C,n) <= (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n) by A1, A5, A7, A9, A8, A4, SPRECT_5:3, XXREAL_0:2; :: thesis: verum