Misc.
Misc.

Follow-up of PR #2344:
* theorem ~pm2.61danel added
* theorem ~nsnlpligALT added
* proof of theorem ~n0lpligALT shortened

Follow-up of PR #2345 :
* comment of ~df-clm adjusted (there was no conjunction missing - it was a parenthesis)
* comments of ~recvs, ~qcvs, ~zclmncvs adjusted (wording of definition/theorems for `ringLMod` used)

metamath/set.mm,metamath/set.mm,metamath/set.mm