theorem RealNon: :: FUZNUM_1:1

for a, b being Real st a <= b holds
REAL \ ].a,b.[ <> {}