for n being Nat holds union (OpenHypercubesRAT n) is open Subset-Family of (TOP-REAL n)