Add faclbnd to iset.mm
Add faclbnd to iset.mm

The theorem is stated as in set.mm. The proof is similar to the
set.mm proof but in one spot real trichotomy needs to be changed to
integer trichotomy.

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