for n being Nat
for a, b, c, d being Element of REAL n st a <= c & d <= b holds
ClosedHyperInterval (c,d) c= ClosedHyperInterval (a,b)