Add toponrestid to set.mm
Add toponrestid to set.mm

This is a convenience theorem from someone on the mailing list (not sure
whether they want to be anonymous or are just saying that credit is not
required).

Minimize 47 theorems with it.

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