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 " and
A3: g is monotone by A1, Def38;
A4: ( f is one-to-one & f is monotone ) by A1, Def38;
then rng f = dom g 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 A4, ORDERS_3:def 5; :: thesis:
assume A5: f . x <= f . y ; :: thesis:
A6: g . (f . x) = x by A2, A4, FUNCT_2:32;
g . (f . y) = y by A2, A4, FUNCT_2:32;
hence x <= y by A3, A5, A6, ORDERS_3:def 5; :: thesis:

end;

assume that
A7: f is one-to-one and
A8: rng f = the carrier of T and
A9: 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 A7; :: 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 A9; :: according to ORDERS_3:def 5 :: thesis:
reconsider g = f " as Function of T,S by A7, A8, 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
A10: a in dom f and
A11: x = f . a by A8, FUNCT_1:def 5;
consider b being set such that
A12: b in dom f and
A13: y = f . b by A8, FUNCT_1:def 5;
reconsider a = a, b = b as Element of S by A10, A12;
A14: g . x = a by A7, A11, FUNCT_2:32;
g . y = b by A7, A13, 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 A9, A11, A13, A14; :: thesis:

end;

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

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

end;