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