let n be 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 Th18;

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:45;

A4: S-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) by A2, SPRECT_2:42;

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-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:39;

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;

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:40;

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:41, 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

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 Th18;

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:45;

A4: S-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) by A2, SPRECT_2:42;

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-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:39;

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;

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:40;

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:41, 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