Metamath Proof Explorer


Syntax definition ct0

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

Ref Expression
Assertion ct0 class Kol2