for A being non empty closed_interval Subset of REAL
for F being FinSequence of bool REAL
for G being FinSequence of ExtREAL st A c= union (rng F) & len F = len G & ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) & ( for n being Nat st n in dom F holds
G . n = diameter (F . n) ) & ( for n being Nat st n in dom F holds
A meets F . n ) holds
diameter A <= Sum G