let A be non empty closed_interval Subset of REAL; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )

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

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:9;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A1, Lm5; :: 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 Lm6; :: thesis: verum

end;

end;

end;

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