let S, T be non empty Poset; :: thesis: ( S,T are_isomorphic iff ex f being monotone Function of S,T ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) )

hereby :: thesis: ( ex f being monotone Function of S,T ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) implies S,T are_isomorphic )

assume S,T are_isomorphic ; :: thesis: ex f being monotone Function of S,T ex g being monotone Function of T,S st
( f * g = id T & g * f = id S )
then consider f being Function of S,T such that
A1: f is isomorphic ;
reconsider f = f as monotone Function of S,T by A1;
consider g being Function of T,S such that
A2: g = f " and
A3: g is monotone by A1, WAYBEL_0:def 38;
take f = f; :: thesis: ex g being monotone Function of T,S st
( f * g = id T & g * f = id S )
reconsider g = g as monotone Function of T,S by A3;
take g = g; :: thesis: ( f * g = id T & g * f = id S )
rng f = the carrier of T by A1, WAYBEL_0:66;
hence ( f * g = id T & g * f = id S ) by A1, A2, FUNCT_2:29; :: thesis: verum

end;

given f being monotone Function of S,T, g being monotone Function of T,S such that A4: f * g = id T and
A5: g * f = id S ; :: thesis: S,T are_isomorphic
take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
A6: f is one-to-one by A5, FUNCT_2:23;
f is onto by A4, FUNCT_2:23;
then rng f = the carrier of T by FUNCT_2:def 3;
then g = f " by A5, A6, FUNCT_2:30;
hence f is isomorphic by A6, WAYBEL_0:def 38; :: thesis: verum