theorem :: SRINGS_5:71

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