theorem :: STRUCT_0:1

for S being non empty ZeroStr
for u being Element of S holds
( u in NonZero S iff not u is zero ) by ZFMISC_1:56;