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 that
A1: f is directed-sups-preserving Function of T,S and
A2: 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
reconsider f = f as Function of T,S by A1;
f is onto by A2, FUNCT_2:23;
hence rng f = the carrier of S by FUNCT_2:def 3; :: thesis: verum