:: deftheorem defines OpenHypercubesRAT SRINGS_5:def 3 :
for n being Nat holds OpenHypercubesRAT n = { (OpenHypercubes q) where q is Point of (Euclid n) : q in RAT n } ;