let n be Element of 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
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A1: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
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 A1, Th3;
hence Lower_Seq C,n is_sequence_on Gauge C,n by JORDAN1E:def 2; :: thesis: verum