:: deftheorem defines Lower_Seq JORDAN1E:def 2 :
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))));