:: deftheorem Def10 defines well-complemented ROBBINS1:def 10 :
for L being non empty OrthoLattStr holds
( L is well-complemented iff for a being Element of L holds a ` is_a_complement_of a );