let L be non empty join-commutative meet-commutative LattStr ; :: thesis: ( L is meet-absorbing implies L is meet-Absorbing )
assume L is meet-absorbing ; :: thesis: L is meet-Absorbing
then for x, y being Element of L holds x "\/" (x "/\" y) = x by LATTICES:def 8;
hence L is meet-Absorbing by ROBBINS3:def 3; :: thesis: verum