set X = {{}};
reconsider SF = {[:{{}},{{}}:]} as Subset-Family of [:{{}},{{}}:] by ZFMISC_1:68;
set US = UniformSpaceStr(# {{}},SF #);
A1: not UniformSpaceStr(# {{}},SF #) is empty ;
UniformSpaceStr(# {{}},SF #) is strict UniformSpace by Th6;
hence not for b₁ being strict UniformSpace holds b₁ is empty by A1; :: thesis: verum