let L, M be non empty RelStr ; :: thesis: ( L,M are_isomorphic & L is transitive implies M is transitive )
assume that
A1: L,M are_isomorphic and
A2: L is transitive ; :: thesis: 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; :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume A4: ( x <= y & y <= z ) ; :: thesis: 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; :: thesis: verum