Metamath Proof Explorer


Syntax definition codu

Description: Class function defining dual orders.

Ref Expression
Assertion codu class ODual