theorem Th9: :: MESFUN14:9

for a, b being Real
for A being non empty closed_interval Subset of REAL
for D being Division of A st A = [.a,b.] holds
ex F being Finite_Sep_Sequence of Borel_Sets st
( dom D = dom F & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) )