let L be 0_Lattice; :: thesis: ( 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 ) ) )
( L is H_Lattice iff L is I_Lattice ) ;
hence ( 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 ) ) ) by FILTER_0:def 6; :: thesis: verum