let L be non empty LattStr ; :: thesis: ( L is meet-Absorbing & L is meet-commutative & L is join-commutative implies L is meet-absorbing )
assume A1: ( L is meet-Absorbing & L is meet-commutative & L is join-commutative ) ; :: thesis: L is meet-absorbing
let a, b be Element of L; :: according to LATTICES:def 8 :: thesis: (a "/\" b) "\/" b = b
b "\/" (b "/\" a) = b by A1, ROBBINS3:def 3;
then b "\/" (a "/\" b) = b by A1, LATTICES:def 6;
hence (a "/\" b) "\/" b = b by A1, LATTICES:def 4; :: thesis: verum