theorem :: SRINGS_5:68

for n being Nat
for a, b being Element of REAL n holds
( OpenHyperInterval (a,b) c= LeftOpenHyperInterval (a,b) & OpenHyperInterval (a,b) c= RightOpenHyperInterval (a,b) & LeftOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) & RightOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) )