set c = {0,1};
set t = {{},{1},{0,1}};
{{},{1},{0,1}} c= bool {0,1}
proof 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