for L being complete LATTICE
for x being Element of L holds meet { I where I is Ideal of L : x <= sup I } = waybelow x