:: deftheorem Def8 defines degenerated STRUCT_0:def 8 :
for S being ZeroOneStr holds
( S is degenerated iff 0. S = 1. S );