( {{} ,{0 }} = bool {0 } & bool {0 } c= bool {0 } ) by ZFMISC_1:30;
then reconsider tau = {{} ,{0 }} as Subset-Family of {0 } ;
reconsider tau = tau as Subset-Family of {0 } ;
0 in {0 } by TARSKI:def 1;
then reconsider r = {[0 ,0 ]} as Relation of {0 } by RELSET_1:8;
take TopRelStr(# {0 },r,tau #) ; :: thesis: ( TopRelStr(# {0 },r,tau #) is strict & 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 finite )
thus ( TopRelStr(# {0 },r,tau #) is strict & 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 finite ) by Lm1; :: thesis: verum