theorem Lm6: :: DIOPHAN1:30

for t being 1 _greater Nat holds (Partial_Union (Equal_Div_interval t)) . (t - 1) = [.0,1.[