:: deftheorem def2 defines pseudocomplemented LATSTONE:def 2 :
for L being non empty LattStr holds
( L is pseudocomplemented iff for x being Element of L ex y being Element of L st y is_a_pseudocomplement_of x );