:: deftheorem def3 defines * LATSTONE:def 3 :
for L being non empty LattStr
for x being Element of L st L is lower-bounded pseudocomplemented Lattice holds
for b₃ being Element of L holds
( b₃ = x * iff b₃ is_a_pseudocomplement_of x );