Metamath Proof Explorer


Syntax definition cmir

Description: Declare the constant for the point inversion function.

Ref Expression
Assertion cmir class pInvG