Metamath Proof Explorer


Syntax definition cconstr

Description: Extend class notation with the set of constructible points.

Ref Expression
Assertion cconstr class Constr