theorem Th4: :: JORDAN1H:4

for r, s being Real st [r,s] in RealOrd holds
r <= s