let n be Nat; :: thesis: for C being compact non horizontal non vertical Subset of () holds (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
let C be compact non horizontal non vertical Subset of (); :: thesis: (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
set Wmi = W-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-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 ;
N-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by ;
then ( 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))))) = (N-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) by ;
hence (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) by ; :: thesis: verum