theorem Th1: :: XXREAL_0:1

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