:: deftheorem D1 defines NonEmptyTrivialUniformSpace UNIFORM2:def 4 :
for b₁ being strict UniformSpaceStr holds
( b₁ = NonEmptyTrivialUniformSpace iff ex SF being Subset-Family of [:{{}},{{}}:] st
( SF = {[:{{}},{{}}:]} & b₁ = UniformSpaceStr(# {{}},SF #) ) );