theorem Th12: :: YELLOW16:13

for T, S being non empty Poset
for f being Function of T,T st f is_a_retraction_of T,S holds
Image f = RelStr(# the carrier of S, the InternalRel of S #)