:: deftheorem Def8 defines `# SHEFFER1:def 8 :
for L being non empty LattStr
for x being Element of L st L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative holds
for b<sub>3</sub> being Element of L holds
( b<sub>3</sub> = x `# iff b₃ is_a_complement'_of x );