theorem Th14: :: YELLOW16:15

for S, T being non empty reflexive transitive RelStr
for f being Function of S,T holds
( f is isomorphic iff ( f is monotone & ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) ) )