:: deftheorem Def7 defines join-idempotent ROBBINS1:def 7 :
for G being non empty \/-SemiLattStr holds
( G is join-idempotent iff for x being Element of G holds x "\/" x = x );