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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} ,{1},{0 ,1}} or x in bool {0 ,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} by XBOOLE_1:2;
hence x in bool {0 ,1} by A2; :: thesis: verum

end;

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

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

end;

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

then x 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