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

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