:: deftheorem Def7 defines complemented' SHEFFER1:def 7 :
for IT being non empty LattStr holds
( IT is complemented' iff for b being Element of IT ex a being Element of IT st a is_a_complement'_of b );