:: deftheorem Def21 defines ` LATTICES:def 21 :
for L being non empty LattStr
for x being Element of L st L is complemented D_Lattice holds
for b<sub>3</sub> being Element of L holds
( b<sub>3</sub> = x ` iff b₃ is_a_complement_of x );