for A being Element of Family_of_Intervals st A is open_interval holds
ex F being Open_Interval_Covering of A st
( F . 0 = A & ( for n being Nat st n <> 0 holds
F . n = {} ) & union (rng F) = A & SUM (F vol) = diameter A )