let L be non empty LattStr ; :: thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies L is meet-absorbing )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; :: thesis: L is meet-absorbing
then A2: ( L is meet-commutative & L is join-commutative ) by Th2;
for x, y being Element of L holds (x "/\" y) "\/" y = y

proof

let a, b be Element of L; :: thesis: (a "/\" b) "\/" b = b
b = b "\/" (b "/\" a) by A1
.= b "\/" (a "/\" b) by A2
.= (a "/\" b) "\/" b by A2 ;
hence (a "/\" b) "\/" b = b ; :: thesis: verum

end;

hence L is meet-absorbing ; :: thesis: verum