Metamath Proof Explorer


Syntax definition ccnrm

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

Ref Expression
Assertion ccnrm class CNrm