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

hence
L is meet-idempotent
; :: thesis: verumlet 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;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