theorem Th1: :: NUMBER03:1

for e1, e2, e3, e4 being ExtReal st e1 <= e2 & e2 <= e3 & e3 <= e4 holds
e1 <= e4