let L be Lattice; :: thesis: the L_meet of L absorbs the L_join of L
let x, y be Element of L; :: according to LATTICE2:def 1 :: thesis: the L_meet of L . x,(the L_join of L . x,y) = x
thus the L_meet of L . x,(the L_join of L . x,y) = x "/\" (x "\/" y)
.= x by LATTICES:def 9 ; :: thesis: verum