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 and
A2: g * f = id S by Th15;
g is isomorphic by A1, A2, Th14;
then A3: g is sups-preserving by WAYBEL13:20;
f is isomorphic by A1, A2, Th14;
then A4: f is sups-preserving by WAYBEL13:20;
then A5: f is_an_UPS_retraction_of S,T by A1, A3;
g is_an_UPS_retraction_of T,S by A2, A4, A3;
hence ( S is_an_UPS_retract_of T & T is_an_UPS_retract_of S ) by A5; :: thesis: verum