:: deftheorem Def1 defines DeMorgan NELSON_1:def 1 :
for L being non empty OrthoLattStr holds
( L is DeMorgan iff for x, y being Element of L holds (x "/\" y) ` = (x `) "\/" (y `) );