let S, T be non empty Poset; ( 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 ( 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
;
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;
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;
( 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;
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
; S,T are_isomorphic
take
f
; WAYBEL_1:def 8 f is isomorphic
A6:
f is V7()
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; verum