Metamath Proof Explorer


Syntax definition ccgrg

Description: Declare the constant for the congruence between shapes relation.

Ref Expression
Assertion ccgrg class 𝒢