for L being non empty Poset
for f being Function of L,L st f is idempotent holds
(corestr f) * (inclusion f) = id (Image f)