Metamath Proof Explorer


Syntax definition cnrm

Description: Extend class notation with the class of all normal topologies.

Ref Expression
Assertion cnrm
class Nrm