for L being complete LATTICE
for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds
( Image f is directed-sups-inheriting & Image f is complete LATTICE )