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 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 )
let r be Relation of {0}; :: thesis: ( tau = {{},{0}} & r = {[0,0]} implies ( 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 ) )
assume that
A1: tau = {{},{0}} and
A2: r = {[0,0]} ; :: 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 finite )
set T = TopRelStr(# {0},r,tau #);
thus TopRelStr(# {0},r,tau #) is trivial ; :: thesis: ( 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 reflexive :: thesis: ( not TopRelStr(# {0},r,tau #) is empty & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite )

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, ORDERS_2:def 9; :: thesis: verum

end;

thus not TopRelStr(# {0},r,tau #) is empty ; :: thesis: ( TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite )
the topology of TopRelStr(# {0},r,tau #) = bool the carrier of TopRelStr(# {0},r,tau #) by A1, ZFMISC_1:30;
hence TopRelStr(# {0},r,tau #) is discrete by TDLAT_3:def 1; :: thesis: TopRelStr(# {0},r,tau #) is finite
thus the carrier of TopRelStr(# {0},r,tau #) is finite ; :: according to STRUCT_0:def 11 :: thesis: verum