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