Metamath Proof Explorer


Syntax definition cline2

Description: Declare the constant for the line function.

Ref Expression
Assertion cline2 class Line