ex SF being Subset-Family of [:{{}},{{}}:] st
( SF = {[:{{}},{{}}:]} & NonEmptyTrivialUniformSpace = UniformSpaceStr(# {{}},SF #) ) by D1;
hence ( not NonEmptyTrivialUniformSpace is empty & not NonEmptyTrivialUniformSpace is void ) ; :: thesis: verum