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 by WAYBEL_1:def 8;
reconsider f = f as monotone Function of S,T by A1;
take f = f; :: thesis: ex g being monotone Function of T,S st
( f * g = id T & g * f = id S )
consider g being Function of T,S such that
A2: ( g = f " & g is monotone ) by A1, WAYBEL_0:def 38;
reconsider g = g as monotone Function of T,S by A2;
take g = g; :: thesis: ( f * g = id T & g * f = id S )
( f is one-to-one & rng f = the carrier of T ) by A1, WAYBEL_0:66;
hence ( f * g = id T & g * f = id S ) by A2, FUNCT_2:35; :: thesis: verum

end;

given f being monotone Function of S,T, g being monotone Function of T,S such that A3: ( f * g = id T & g * f = id S ) ; :: thesis: S,T are_isomorphic
take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
A4: ( f is one-to-one & rng f = the carrier of T ) by A3, FUNCT_2:29;
then g = f " by A3, FUNCT_2:36;
hence f is isomorphic by A4, WAYBEL_0:def 38; :: thesis: verum