Metamath Proof Explorer


Syntax definition cthl

Description: Extend class notation with the Hilbert lattice.

Ref Expression
Assertion cthl class toHL