Metamath Proof Explorer


Syntax definition cph

Description: Extend class notation with subspace sum in CH .

Ref Expression
Assertion cph class +