Metamath Proof Explorer


Syntax definition chlg

Description: Function producing the relation "belong to the same half-line".

Ref Expression
Assertion chlg class hl 𝒢