:: deftheorem defines is_a_pseudocomplement_of LATSTONE:def 1 :
for L being non empty LattStr
for a, b being Element of L holds
( a is_a_pseudocomplement_of b iff ( a "/\" b = Bottom L & ( for x being Element of L st b "/\" x = Bottom L holds
x [= a ) ) );