theorem Th1: :: RFUNCT_4:1

for a, b being Real holds max (a,b) >= min (a,b)