theorem Th18: :: YELLOW16:19

for T being non empty up-complete Poset
for S being non empty Poset
for f being Function st f is_an_UPS_retraction_of T,S holds
ex h being directed-sups-preserving projection Function of T,T st
( h is_a_retraction_of T, Image h & S, Image h are_isomorphic )