let L be non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: L is meet-idempotent
now :: thesis: for x being Element of L holds x "/\" x = x
let x be Element of L; :: thesis: x "/\" x = x
thus x "/\" x = (x "/\" x) "\/" (Bot' L) by Def4
.= (x "/\" x) "\/" (x "/\" (x `#)) by Th3
.= x "/\" (x "\/" (x `#)) by LATTICES:def 11
.= x "/\" (Top' L) by Th2
.= x by Def2 ; :: thesis: verum
end;
hence L is meet-idempotent ; :: thesis: verum