let n be Nat; 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); 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; verum