let L, M be non empty RelStr ; ( L,M are_isomorphic & L is transitive implies M is transitive )
assume that
A1:
L,M are_isomorphic
and
A2:
L is transitive
; M is transitive
M,L are_isomorphic
by A1, WAYBEL_1:6;
then consider f being Function of M,L such that
A3:
f is isomorphic
;
let x, y, z be Element of M; YELLOW_0:def 2 ( not x <= y or not y <= z or x <= z )
assume A4:
( x <= y & y <= z )
; x <= z
reconsider fz = f . z as Element of L ;
reconsider fy = f . y as Element of L ;
reconsider fx = f . x as Element of L ;
( fx <= fy & fy <= fz )
by A3, A4, WAYBEL_0:66;
then
fx <= fz
by A2;
hence
x <= z
by A3, WAYBEL_0:66; verum