( 2 c= 3 & card 2 = 2 ) by CARD_1:def 2, NAT_1:39;
then consider K being Subset of 3 such that
A1: card K = 2 ;
{ 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 } \ {K} as Subset-Family of 3 by XBOOLE_1:1;
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 & 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 c= 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 & 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 A1, Th8; :: thesis: verum