Suggestion: TopRealAsSynonym

Replace http://megrez.mizar.org/cgi-bin/meaning.cgi?entry=EUCLID:def.8

with a synonym TOP-REAL n for TopSpaceMetr (Euclid n)

the strictness is then automatic, the TopSpace can be stated as a cluster.

This will save a lot of pain to those who have to cast Subset of TOP-REAL n to Subset of TopSpaceMetr (Euclid n) and vice-versa all the time

Follow up

AdamGrabowski just observed that such general synonyms are not possible :-(. I posted some suggestions to MizarForum : http://mizar.uwb.edu.pl/forum/archive/0404/msg00004.html