let A be closed-interval Subset of REAL ; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )

now

per cases ( vol A <> 0 or vol A = 0 ) ;

suppose A1: vol A <> 0 ; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )

vol A >= 0 by INTEGRA1:11;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A1, Lm4; :: thesis: verum

end;

suppose vol A = 0 ; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )

hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by Lm5; :: thesis: verum

end;

end;

end;

hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: verum