:: deftheorem defines is_a_retraction_of YELLOW16:def 1 :
for S, T being non empty Poset
for f being Function holds
( f is_a_retraction_of T,S iff ( f is directed-sups-preserving Function of T,S & f | the carrier of S = id S & S is full directed-sups-inheriting SubRelStr of T ) );