Metamath Proof Explorer


Syntax definition cmid

Description: Declare the constant for the midpoint operation.

Ref Expression
Assertion cmid class mid 𝒢