theorem Th9: :: YELLOW16:10

for S, T being non empty Poset
for f being Function st f is_a_retraction_of T,S holds
rng f = the carrier of S