let n be Nat; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )
set x = S-min (L~ (Cage (C,n)));
set p = E-max (L~ (Cage (C,n)));
set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
A1: rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = rng (Cage (C,n)) by FINSEQ_6:90, SPRECT_2:43;
A2: S-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:41;
A3: (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by JORDAN1F:5;
A4: L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A5: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
A6: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) by JORDAN1E:def 1;
then A7: (Upper_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by A5, FINSEQ_5:44;
then A8: (E-max (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < (E-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A4, JORDAN1F:5, SPRECT_5:26;
A9: (E-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (S-max (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A7, A4, JORDAN1F:5, SPRECT_5:27;

per cases ( S-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <> W-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) or S-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) = W-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) ) ;

suppose S-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <> W-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) ; :: thesis: ( S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

then (E-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < (S-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A7, A3, A4, A9, SPRECT_5:28, XXREAL_0:2;
then S-min (L~ (Cage (C,n))) in rng ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) by A1, A2, A6, A4, A8, FINSEQ_6:62, XXREAL_0:2;
hence A10: S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by JORDAN1E:def 2; :: thesis: S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n))
len (Lower_Seq (C,n)) >= 2 by TOPREAL1:def 8;
then rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n)) by SPPOL_2:18;
hence S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) by A10; :: thesis: verum

end;

suppose A11: S-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) = W-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) ; :: thesis: ( S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )

(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) by JORDAN1F:8;
hence A12: S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by A4, A11, FINSEQ_6:168; :: thesis: S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n))
len (Lower_Seq (C,n)) >= 2 by TOPREAL1:def 8;
then rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n)) by SPPOL_2:18;
hence S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) by A12; :: thesis: verum

end;

end;