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