Metamath Proof Explorer


Syntax definition clvol

Description: Extend class notation with set of all 3-dimensional "lattice volumes" (lattice elements which cover a plane) in a Hilbert lattice.

Ref Expression
Assertion clvol class LVols