:: deftheorem Def6 defines with_non_trivial_blocks PENCIL_1:def 6 :
for S being TopStruct holds
( S is with_non_trivial_blocks iff for k being Block of S holds 2 c= card k );