let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds Upper_Seq C,n is_sequence_on Gauge C,n
let n be Element of NAT ; :: 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 A1: Rotate (Cage C,n),(W-min (L~ (Cage C,n))) is_sequence_on Gauge C,n by REVROT_1:34;
Upper_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n))) by JORDAN1E:def 1
.= (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 FINSEQ_5:def 1 ;
hence Upper_Seq C,n is_sequence_on Gauge C,n by A1, GOBOARD1:38; :: thesis: verum