Metamath Proof Explorer


Syntax definition clines

Description: Extend class notation with set of all projective lines for a Hilbert lattice.

Ref Expression
Assertion clines
class Lines