Fix reverse closure text in iset conventions

To say reverse closure is not possible in iset.mm is too oversimplified,
as set.mm uses the phrase "reverse closure" for various theorems.
Some intuitionize, some don't.  So be a bit more specific and point to
relelfvdm as another way out.

Author: jkingdon

iset.mm

@@ -136310,10 +136310,12 @@ Metamath Proof Explorer (MPE, set.mm).  This list of conventions is
        its domain, the same result follows.  Since the function must
        be evaluated within its domain or outside it, the result follows
        unconditionally" (the use of excluded middle in this argument is
-       perhaps obvious when stated this way).  For this reason, we
-       generally need to prove we are evaluating functions within
-       their domains and avoid the reverse closure theorems of the
-       Metamath Proof Explorer.</li>
+       perhaps obvious when stated this way).  Often, the easiest fix
+       will be to prove we are evaluating functions within
+       their domains, other times it will be possible to use a theorem
+       like ~ relelfvdm which says that if a function value produces
+       an inhabited set, then the function is being evaluated within
+       its domain.</li>
 
        <li><b>Bibliography references.</b>
        The bibliography for the Intuitionistic Logic Explorer is