theorem Th1: :: XREAL_1:1

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