0 in {0} by TARSKI:def 1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:8;
{{},{0}} = bool {0} by ZFMISC_1:30;
then reconsider tau = {{},{0}} as Subset-Family of {0} ;
take TopRelStr(# {0},r,tau #) ; :: thesis: ( TopRelStr(# {0},r,tau #) is trivial & TopRelStr(# {0},r,tau #) is reflexive & not TopRelStr(# {0},r,tau #) is empty & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is strict & TopRelStr(# {0},r,tau #) is finite )
thus ( TopRelStr(# {0},r,tau #) is trivial & TopRelStr(# {0},r,tau #) is reflexive & not TopRelStr(# {0},r,tau #) is empty & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is strict & TopRelStr(# {0},r,tau #) is finite ) by Lm4; :: thesis: verum