theorem :: LATTICE2:67

for L being 0_Lattice holds
( L is H_Lattice iff for x, z being Element of L ex y being Element of L st
( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds
v [= y ) ) )