let S be non empty ZeroStr ; :: thesis: for u being Element of S holds
( u in NonZero S iff not u is zero )
let u be Element of S; :: thesis: ( u in NonZero S iff not u is zero )
thus ( u in NonZero S implies not u is zero ) :: thesis: ( not u is zero implies u in NonZero S )

proof

assume u in NonZero S ; :: thesis: not u is zero
then u <> 0. S by ZFMISC_1:64;
hence not u is zero by Def12; :: thesis: verum

end;

thus ( not u is zero implies u in NonZero S ) :: thesis: verum

proof

assume not u is zero ; :: thesis: u in NonZero S
then u <> 0. S by Def12;
hence u in NonZero S by ZFMISC_1:64; :: thesis: verum

end;