for S, T being non empty Poset holds
( 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 ) )