theorem Th10: :: WAYBEL27:10

for S, T being complete LATTICE
for f being idempotent Function of T,T
for h being Function of S,(Image f) holds f * h = h