theorem th28: :: DBLSEQ_1:1

for a, b, c being Real st a <= b & b <= c & not |.b.| <= |.a.| holds
|.b.| <= |.c.|