Metamath Proof Explorer


Syntax definition cocv

Description: Extend class notation with orthocomplement of a subset.

Ref Expression
Assertion cocv class ocv