Full reorganization of the mathbox using subsections, following Gerard Lang's advice
Full reorganization of the mathbox using subsections, following Gerard Lang's advice

Also:
- some rewording in the Uniform Structure section,
- added a proof for “ ` RR ` is a complete uniform space”.

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