Metamath Proof Explorer


Syntax definition cprstc

Description: Class function defining preordered sets as categories.

Ref Expression
Assertion cprstc
class ProsetToCat