for L being lower-bounded meet-continuous LATTICE
for x being Element of L holds meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } = waybelow x