( Segm 2 c= Segm 3 & card 2 = 2 ) by 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 object ; :: 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 (Segm 3) : 2 = card L } \ {K} as Subset-Family of (Segm 3) by XBOOLE_1:1;
take TopStruct(# (Segm 3),B #) ; :: thesis: ( TopStruct(# (Segm 3),B #) is strict & not TopStruct(# (Segm 3),B #) is empty & not TopStruct(# (Segm 3),B #) is void & not TopStruct(# (Segm 3),B #) is degenerated & TopStruct(# (Segm 3),B #) is truly-partial & TopStruct(# (Segm 3),B #) is with_non_trivial_blocks & TopStruct(# (Segm 3),B #) is identifying_close_blocks & TopStruct(# (Segm 3),B #) is without_isolated_points )
3 c= card 3 ;
then for K being Subset of (Segm 3) st card K = 2 holds
for S being TopStruct st the carrier of S = Segm 3 & the topology of S = { L where L is Subset of (Segm 3) : 2 = card L } \ {K} holds
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) by Th8;
hence ( TopStruct(# (Segm 3),B #) is strict & not TopStruct(# (Segm 3),B #) is empty & not TopStruct(# (Segm 3),B #) is void & not TopStruct(# (Segm 3),B #) is degenerated & TopStruct(# (Segm 3),B #) is truly-partial & TopStruct(# (Segm 3),B #) is with_non_trivial_blocks & TopStruct(# (Segm 3),B #) is identifying_close_blocks & TopStruct(# (Segm 3),B #) is without_isolated_points ) by A1; :: thesis: verum