theorem :: STRUCT_0:3

for S being ZeroStr holds not 0. S in NonZero S