theorem Th26: :: EUCLID_9:26

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