Correct comment of sqrt2irr in iset.mm
Correct comment of sqrt2irr in iset.mm

What we prove here is that the square root of 2 is not rational. Offer a
few sentences about the difference between that and irrational (given
the usual definition of "irrational" in the absence of excluded middle).

Given that, don't claim this as a theorem for metamath 100 for iset.mm.

Tweak a few other uses of the word "irrational" which don't make sense
given this.

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