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