:: deftheorem defines is_an_UPS_retract_of YELLOW16:def 4 :
for S, T being non empty Poset holds
( S is_an_UPS_retract_of T iff ex f being Function of T,S st f is_an_UPS_retraction_of T,S );