{} (bool the carrier of T) is open ;
hence ex b₁ being Subset-Family of T st
( b₁ is countable & b₁ is open & b₁ is closed ) ; :: thesis: verum