theorem Th33: :: WAYBEL_1:33

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)