Metamath Proof Explorer


Syntax definition cpointsN

Description: Extend class notation with set of all projective points.

Ref Expression
Assertion cpointsN
class Points