Metamath Proof Explorer


Syntax definition cphl

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

Ref Expression
Assertion cphl class PreHil