Metamath Proof Explorer

Syntax definition club

Description: Extend class notation with poset least upper bound.

Ref Expression
Assertion club class lub