:: deftheorem defines with_idempotent_element ROBBINS1:def 13 :
for G being non empty ComplLLattStr holds
( G is with_idempotent_element iff ex x being Element of G st x + x = x );