Metamath Proof Explorer


Syntax definition clmi

Description: Declare the constant for the line mirroring function.

Ref Expression
Assertion clmi class lInvG