set c = {0,1};
set t = {{},{1},{0,1}};
{{},{1},{0,1}} c= bool {0,1}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{},{1},{0,1}} or x in bool {0,1} )
reconsider xx = x as set by TARSKI:1;
assume A1: x in {{},{1},{0,1}} ; :: thesis: x in bool {0,1}

per cases ( x = {} or x = {1} or x = {0,1} ) by A1, ENUMSET1:def 1;

suppose A2: x = {} ; :: thesis: x in bool {0,1}

{} c= {0,1} ;
hence x in bool {0,1} by A2; :: thesis: verum

end;

suppose x = {1} ; :: thesis: x in bool {0,1}

then xx c= {0,1} by ZFMISC_1:7;
hence x in bool {0,1} ; :: thesis: verum

end;

suppose x = {0,1} ; :: thesis: x in bool {0,1}

then xx c= {0,1} ;
hence x in bool {0,1} ; :: thesis: verum

end;

end;

end;

then reconsider t = {{},{1},{0,1}} as Subset-Family of {0,1} ;
take s = TopStruct(# {0,1},t #); :: thesis: ( the carrier of s = {0,1} & the topology of s = {{},{1},{0,1}} )
thus the carrier of s = {0,1} ; :: thesis: the topology of s = {{},{1},{0,1}}
thus the topology of s = {{},{1},{0,1}} ; :: thesis: verum