Metamath Proof Explorer


Syntax definition cha

Description: Extend class notation with the class of all Hausdorff spaces.

Ref Expression
Assertion cha class Haus