let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: L is join-absorbing
let x, y be Element of L; :: according to LATTICES:def 9 :: thesis: x "/\" (x "\/" y) = x
A1: L is meet-idempotent by Th8;
A2: L is meet-absorbing by Th10;
x "/\" (x "\/" y) = (x "/\" x) "\/" (x "/\" y) by LATTICES:def 11
.= x "\/" (x "/\" y) by A1
.= x by A2 ;
hence x "/\" (x "\/" y) = x ; :: thesis: verum