Metamath Proof Explorer

Syntax definition cprstc

Description: Class function defining preordered sets as categories.

Ref Expression
Assertion cprstc class ProsetToCat