let S, T be non empty up-complete Poset; :: thesis: ( S,T are_isomorphic implies ( S is_an_UPS_retract_of T & T is_an_UPS_retract_of S ) )
assume S,T are_isomorphic ; :: thesis: ( S is_an_UPS_retract_of T & T is_an_UPS_retract_of S )
then consider f being monotone Function of S,T, g being monotone Function of T,S such that
A1: ( f * g = id T & g * f = id S ) by Th18;
( f is isomorphic & g is isomorphic ) by A1, Th17;
then ( f is sups-preserving & g is sups-preserving ) by WAYBEL13:20;
then ( ( for X being Subset of S st not X is empty & X is directed holds
f preserves_sup_of X ) & ( for X being Subset of T st not X is empty & X is directed holds
g preserves_sup_of X ) ) by WAYBEL_0:def 33;
then ( f is directed-sups-preserving & g is directed-sups-preserving ) by WAYBEL_0:def 37;
then ( g is_an_UPS_retraction_of T,S & f is_an_UPS_retraction_of S,T ) by A1, Def2;
hence ( S is_an_UPS_retract_of T & T is_an_UPS_retract_of S ) by Def4; :: thesis: verum