:: deftheorem defines is_an_UPS_retraction_of YELLOW16:def 2 :
for S, T being non empty Poset
for f being Function holds
( f is_an_UPS_retraction_of T,S iff ( f is directed-sups-preserving Function of T,S & ex g being directed-sups-preserving Function of S,T st f * g = id S ) );