for n being Nat
for a, b being Element of REAL n st b < a & not n is zero holds
ClosedHyperInterval (a,b) is empty