:: deftheorem defines dense_countable_OpenHypercubes SRINGS_5:def 6 :
for n being Nat holds dense_countable_OpenHypercubes n = union (OpenHypercubesRAT n);