Metamath Proof Explorer


Syntax definition ccgra

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

Ref Expression
Assertion ccgra class cgrA