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