:: deftheorem Def2 defines divs INTEGRA1:def 3 :
for A being non empty compact Subset of REAL
for b₂ being set holds
( b₂ = divs A iff for x1 being set holds
( x1 in b₂ iff x1 is Division of A ) );