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