( dense_countable_OpenHypercubes n is Basis of (TOP-REAL n) & dense_countable_OpenHypercubes n is countable ) by Th21;
hence ex b₁ being Basis of (TOP-REAL n) st b₁ is countable ; :: thesis: verum