let L be non empty ComplLLattStr ; :: thesis: ( L is join-commutative & L is join-associative & L is Huntington implies L is join-idempotent )
assume ( L is join-commutative & L is join-associative & L is Huntington ) ; :: thesis: L is join-idempotent
then for a being Element of L holds a + a = a by Th13;
hence L is join-idempotent by Def7; :: thesis: verum