let S, T be non empty up-complete Poset; ( S,T are_isomorphic implies ( S is_an_UPS_retract_of T & T is_an_UPS_retract_of S ) )
assume
S,T are_isomorphic
; ( 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; verum