for seq being Real_Sequence holds
( seq is convergent & lim seq = 0 iff ( abs seq is convergent & lim (abs seq) = 0 ) )