consider a being NonUnit of R such that
H: a <> 0. R by lemf;
not a is zero by H;
hence not for b₁ being NonUnit of R holds b₁ is zero ; :: thesis: verum