Step
*
of Lemma
lattice-meet-1
∀[l:BoundedLattice]. ∀[x:Point(l)]. (x ∧ 1 = x ∈ Point(l))
BY
{ Auto }
1
1. l : BoundedLattice
2. x : Point(l)
⊢ x ∧ 1 = x ∈ Point(l)
Latex:
Latex:
\mforall{}[l:BoundedLattice]. \mforall{}[x:Point(l)]. (x \mwedge{} 1 = x)
By
Latex:
Auto
Home
Index