Metamath Proof Explorer


Syntax definition clines2

Description: Declare the constant for the set of all lines.

Ref Expression
Assertion clines2
class LinesEE