for T being TopSpace
for K being Subset-Family of T holds
( K is Basis of T iff K \ {{}} is Basis of T )