Metamath Proof Explorer


Syntax definition cplt

Description: Extend class notation with less-than for posets.

Ref Expression
Assertion cplt class lt