theorem Th2: :: XREAL_1:2

for a being Real ex b being Real st b < a