:: deftheorem Def2 defines Lower_Appr JORDAN19:def 2 :
for C being Simple_closed_curve
for b₂ being SetSequence of the carrier of (TOP-REAL 2) holds
( b₂ = Lower_Appr C iff for i being Nat holds b₂ . i = Lower_Arc (L~ (Cage (C,i))) );