theorem Th27: :: EUCLID_9:27

for n being Nat
for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is open