let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq (C,n) is_sequence_on Gauge (C,n)
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: Lower_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;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
then (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) is_sequence_on Gauge (C,n) by A1, Th3;
hence Lower_Seq (C,n) is_sequence_on Gauge (C,n) by JORDAN1E:def 2; :: thesis: verum