:: deftheorem defines PseudoComplements LATTICEA:def 8 :
for L being Lattice
for a being Element of L holds PseudoComplements a = { x where x is Element of L : a "/\" x = Bottom L } ;