:: deftheorem defines Dneg OPOSET_1:def 3 :
for O being non empty OrthoRelStr holds
( O is Dneg iff ex f being Function of O,O st
( f = the Compl of O & f is V256() ) );