for X being set
for B being B_Lattice
for a being Element of B holds
( X is_greater_than a iff { (b `) where b is Element of B : b in X } is_less_than a ` )