{ L where L is Subset of 3 : 2 = card L } c= bool 3

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { L where L is Subset of 3 : 2 = card L } or x in bool 3 )
assume x in { L where L is Subset of 3 : 2 = card L } ; :: thesis: x in bool 3
then ex L being Subset of 3 st
( x = L & 2 = card L ) ;
hence x in bool 3 ; :: thesis: verum

end;

then reconsider B = { L where L is Subset of 3 : 2 = card L } as Subset-Family of 3 ;
take TopStruct(# 3,B #) ; :: thesis: ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & not TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points )
3 = card 3 by CARD_1:def 2;
hence ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & not TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points ) by Th7; :: thesis: verum