let L be Lattice; :: thesis: ( L is join-idempotent & L is meet-idempotent )
for x being Element of L holds x "\/" x = x ;
hence L is join-idempotent by ROBBINS1:def 7; :: thesis: L is meet-idempotent
for x being Element of L holds x "/\" x = x ;
hence L is meet-idempotent by SHEFFER1:def 9; :: thesis: verum