:: deftheorem defines is_a_retract_of YELLOW16:def 3 :
for S, T being non empty Poset holds
( S is_a_retract_of T iff ex f being Function of T,S st f is_a_retraction_of T,S );