Shorten set.mm proof of fzm1
Shorten set.mm proof of fzm1

This is the proof I came up with for iset.mm and it is
814 characters whereas the previous one was 1043 characters.

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