:: deftheorem Def1 defines Division INTEGRA1:def 2 :
for A being non empty compact Subset of REAL
for b₂ being non empty increasing FinSequence of REAL holds
( b₂ is Division of A iff ( rng b₂ c= A & b₂ . (len b₂) = upper_bound A ) );