let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq C,n is_sequence_on Gauge C,n
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: Upper_Seq C,n is_sequence_on Gauge C,n
Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
then Rotate (Cage C,n),(W-min (L~ (Cage C,n))) is_sequence_on Gauge C,n by REVROT_1:34;
then (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n))) is_sequence_on Gauge C,n by Th2;
hence Upper_Seq C,n is_sequence_on Gauge C,n by JORDAN1E:def 1; :: thesis: verum