let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( W-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) & W-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( W-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) & W-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
set x = W-max (L~ (Cage C,n));
set p = W-min (L~ (Cage C,n));
set f = Rotate (Cage C,n),(E-max (L~ (Cage C,n)));
A1: rng (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) = rng (Cage C,n) by FINSEQ_6:96, SPRECT_2:50;
A2: W-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:48;
A3: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
A4: Lower_Seq C,n = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) -: (W-min (L~ (Cage C,n))) by JORDAN1G:26;
W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then W-min (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:50;
then A5: (Lower_Seq C,n) /. 1 = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 1 by A4, FINSEQ_5:47;
A6: L~ (Cage C,n) = L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by REVROT_1:33;
then (W-min (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) < (W-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A5, JORDAN1F:6, SPRECT_5:43;
then W-max (L~ (Cage C,n)) in rng ((Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) :- (W-min (L~ (Cage C,n)))) by A1, A2, A3, A6, FINSEQ_6:67;
hence A7: W-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) by Th4; :: thesis: W-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n)
len (Upper_Seq C,n) >= 2 by TOPREAL1:def 10;
then rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by SPPOL_2:18;
hence W-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) by A7; :: thesis: verum