let L be non empty up-complete Poset; :: thesis: for S being non empty Poset st S is_an_UPS_retract_of L holds
S is up-complete
let S be non empty Poset; :: thesis: ( S is_an_UPS_retract_of L implies S is up-complete )
given f being Function of L,S such that A1: f is_an_UPS_retraction_of L,S ; :: according to YELLOW16:def 4 :: thesis: S is up-complete
consider h being directed-sups-preserving projection Function of L,L such that
A2: ( h is_a_retraction_of L, Image h & S, Image h are_isomorphic ) by A1, Th21;
h = corestr h by WAYBEL_1:32;
then Image h is_a_retract_of L by A2, Def3;
then ( Image h is up-complete & Image h,S are_isomorphic ) by A2, Th22, WAYBEL_1:7;
hence S is up-complete by WAYBEL13:30; :: thesis: verum