theorem Th61: :: MEASUR12:61

for F being non empty disjoint_valued FinSequence of Family_of_Intervals st Union F is Interval holds
ex n being Nat st
( n in dom F & (Union F) \ (F . n) is Interval )