:: deftheorem defines PseudoCocomplements LATTICEA:def 9 :
for L being Lattice
for a being Element of L holds PseudoCocomplements a = { x where x is Element of L : a "\/" x = Top L } ;