for L being complete LATTICE
for x being Element of L holds meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x