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

A3: W-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, SPRECT_2:44;

A4: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, SPRECT_2:46;

W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

then A5: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_6:92;

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

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

(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:24;

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:23, 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:25, 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

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

A3: W-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, SPRECT_2:44;

A4: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, SPRECT_2:46;

W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

then A5: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_6:92;

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

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

(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:24;

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:23, 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:25, 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