let n be Element of 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:96, SPRECT_2:47;
A2: S-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:45;
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:50;
then A5: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
A6: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
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:47;
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:27;
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:28;

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:29, 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:67, 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 10;
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, REVROT_1:3; :: thesis: S-min (L~ (Cage C,n)) in L~ (Lower_Seq C,n)
len (Lower_Seq C,n) >= 2 by TOPREAL1:def 10;
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;