Metamath Proof Explorer

Syntax definition chil

Description: Extend class notation with class of all Hilbert spaces.

Ref Expression
Assertion chil class Hil