:: deftheorem defines degenerated PENCIL_1:def 5 :
for S being TopStruct holds
( S is degenerated iff the carrier of S is Block of S );