theorem :: INTEGRA1:32

for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D holds
ex A1, A2 being non empty closed_interval Subset of REAL st
( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )