:: deftheorem Def7 defines identifying_close_blocks PENCIL_1:def 7 :
for S being TopStruct holds
( S is identifying_close_blocks iff for k, l being Block of S st 2 c= card (k /\ l) holds
k = l );