theorem :: LATTICE3:23

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