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