:: deftheorem defines meet-idempotent SHEFFER1:def 9 :
for G being non empty /\-SemiLattStr holds
( G is meet-idempotent iff for x being Element of G holds x "/\" x = x );