set X = {{}};
reconsider SF = {[:{{}},{{}}:]} as Subset-Family of [:{{}},{{}}:] by ZFMISC_1:68;
take UniformSpaceStr(# {{}},SF #) ; :: thesis: ex SF being Subset-Family of [:{{}},{{}}:] st
( SF = {[:{{}},{{}}:]} & UniformSpaceStr(# {{}},SF #) = UniformSpaceStr(# {{}},SF #) )
thus ex SF being Subset-Family of [:{{}},{{}}:] st
( SF = {[:{{}},{{}}:]} & UniformSpaceStr(# {{}},SF #) = UniformSpaceStr(# {{}},SF #) ) ; :: thesis: verum