Metamath Proof Explorer


Syntax definition cordt

Description: Extend class notation with the order topology.

Ref Expression
Assertion cordt class ordTop