let S, T be non empty Poset; :: thesis: for f being Function st f is_an_UPS_retraction_of T,S holds
rng f = the carrier of S
let f be Function; :: thesis: ( f is_an_UPS_retraction_of T,S implies rng f = the carrier of S )
assume ( f is directed-sups-preserving Function of T,S & ex g being directed-sups-preserving Function of S,T st f * g = id S ) ; :: according to YELLOW16:def 2 :: thesis: rng f = the carrier of S
hence rng f = the carrier of S by FUNCT_2:29; :: thesis: verum