let S, T be non empty RelStr ; :: thesis:
let f be Function of S,T; :: thesis:

hereby :: thesis:

assume A1: f is isomorphic ; :: thesis:
hence f is one-to-one by Def38; :: thesis:
consider g being Function of T,S such that
A2: ( g = f " & g is monotone ) by A1, Def38;
A3: ( f is one-to-one & f is monotone ) by A1, Def38;
then ( rng f = dom g & g is Function of the carrier of T,the carrier of S ) by A2, FUNCT_1:55;
hence rng f = the carrier of T by FUNCT_2:def 1; :: thesis:
let x, y be Element of S; :: thesis:
thus ( x <= y implies f . x <= f . y ) by A3, ORDERS_3:def 5; :: thesis:
assume A4: f . x <= f . y ; :: thesis:
( g . (f . x) = x & g . (f . y) = y ) by A2, A3, FUNCT_2:32;
hence x <= y by A2, A4, ORDERS_3:def 5; :: thesis:

end;

assume A5: ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) ; :: thesis:

per cases ;
:: according to WAYBEL_0:def 38

case ( not S is empty & not T is empty ) ; :: thesis:

thus f is one-to-one by A5; :: thesis:
thus for x, y being Element of S st x <= y holds
for a, b being Element of T st a = f . x & b = f . y holds
a <= b by A5; :: according to ORDERS_3:def 5 :: thesis:
reconsider g = f " as Function of T,S by A5, FUNCT_2:31;
take g ; :: thesis:
thus g = f " ; :: thesis:
let x, y be Element of T; :: according to ORDERS_3:def 5 :: thesis:
consider a being set such that
A6: ( a in dom f & x = f . a ) by A5, FUNCT_1:def 5;
consider b being set such that
A7: ( b in dom f & y = f . b ) by A5, FUNCT_1:def 5;
reconsider a = a, b = b as Element of S by A6, A7;
( g . x = a & g . y = b ) by A5, A6, A7, FUNCT_2:32;
hence ( not x <= y or for b₁, b₂ being Element of the carrier of S holds
( not b₁ = g . x or not b₂ = g . y or b₁ <= b₂ ) ) by A5, A6, A7; :: thesis:

end;

case ( S is empty or T is empty ) ; :: thesis:

hence ( S is empty & T is empty ) ; :: thesis:

end;