:: deftheorem Def3 defines divset INTEGRA1:def 4 :
for A being non empty closed_interval Subset of REAL
for D being Division of A
for i being Nat st i in dom D holds
for b₄ being non empty closed_interval Subset of REAL holds
( ( i = 1 implies ( b₄ = divset (D,i) iff ( lower_bound b₄ = lower_bound A & upper_bound b₄ = D . i ) ) ) & ( not i = 1 implies ( b₄ = divset (D,i) iff ( lower_bound b₄ = D . (i - 1) & upper_bound b₄ = D . i ) ) ) );