Metamath Proof Explorer


Syntax definition cdir

Description: Extend class notation with the class of directed sets.

Ref Expression
Assertion cdir class DirRel