let L be non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: L is join-idempotent
let x be Element of L; :: according to ROBBINS1:def 7 :: thesis: x "\/" x = x
thus x "\/" x = (x "\/" x) "/\" (Top' L) by Def2
.= (x "\/" x) "/\" (x "\/" (x `#)) by Th2
.= x "\/" (x "/\" (x `#)) by Def5
.= x "\/" (Bot' L) by Th3
.= x by Def4 ; :: thesis: verum