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

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