Metamath Proof Explorer

Syntax definition cordt

Description: Extend class notation with the order topology.

Ref Expression
Assertion cordt class ordTop