let tau be Subset-Family of {0}; :: thesis: for r being Relation of {0} st tau = {{},{0}} & r = {[0,0]} holds
( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
let r be Relation of {0}; :: thesis: ( tau = {{},{0}} & r = {[0,0]} implies ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) )
assume that
A1: tau = {{},{0}} and
A2: r = {[0,0]} ; :: thesis: ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
set T = TopRelStr(# {0},r,tau #);
thus TopRelStr(# {0},r,tau #) is reflexive :: thesis: ( TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )

proof

let x be Element of TopRelStr(# {0},r,tau #); :: according to YELLOW_0:def 1 :: thesis: x <= x
x = 0 by TARSKI:def 1;
then [x,x] in {[0,0]} by TARSKI:def 1;
hence x <= x by A2; :: thesis: verum

end;

the topology of TopRelStr(# {0},r,tau #) = bool the carrier of TopRelStr(# {0},r,tau #) by A1, ZFMISC_1:24;
hence TopRelStr(# {0},r,tau #) is discrete by TDLAT_3:def 1; :: thesis: ( TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
thus ( TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) ; :: thesis: verum