let a be non zero Element of R; :: thesis: not a is nilpotent
a <> 0. R ;
hence not a is nilpotent by NIL1; :: thesis: verum