let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); (E-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) < (E-min (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 Th18;
A2:
L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = L~ (Cage (C,n))
by REVROT_1:33;
then A3:
E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by SPRECT_2:46;
A4:
E-min (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by A2, SPRECT_2:45;
A5:
W-min (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by A2, SPRECT_2:43;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:46;
then A6:
(Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. 1 = E-max (L~ (Cage (C,n)))
by FINSEQ_6:92;
then A7:
(E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) < (E-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by A2, SPRECT_5:37;
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:41;
(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:40;
then A9:
(E-min (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:39, 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)))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))))
by A2, A6, SPRECT_5:41, XXREAL_0:2;
then
(E-max (L~ (Cage (C,n)))) .. ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))) = (E-max (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-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
by A1, A5, A7, A8, A9, A4, SPRECT_5:3, XXREAL_0:2; verum