theorem Th2: :: XXREAL_0:2

for a, b, c being ExtReal st a <= b & b <= c holds
a <= c