for L being complete LATTICE
for x being Element of L holds (L -waybelow) -below x = waybelow x