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