Metamath Proof Explorer


Syntax definition cp0

Description: Extend class notation with poset zero.

Ref Expression
Assertion cp0
class 0.