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

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