Metamath Proof Explorer


Syntax definition cordt

Description: Extend class notation with the order topology.

Ref Expression
Assertion cordt
class ordTop