let R, S be RelStr ; :: thesis: ( R,S are_isomorphic & R is Dickson & R is quasi_ordered implies ( S is quasi_ordered & S is Dickson ) )
assume that
A1: R,S are_isomorphic and
A2: R is Dickson and
A3: R is quasi_ordered ; :: thesis: ( S is quasi_ordered & S is Dickson )
set CRS = the carrier of S;
set IRS = the InternalRel of S;

per cases ( ( not R is empty & not S is empty ) or R is empty or S is empty ) ;

suppose ( not R is empty & not S is empty ) ; :: thesis: ( S is quasi_ordered & S is Dickson )

then reconsider Re = R, Se = S as non empty RelStr ;
consider f being Function of Re,Se such that
A4: f is isomorphic by A1, WAYBEL_1:def 8;
A5: ( f is one-to-one & rng f = the carrier of Se & ( for x, y being Element of Re holds
( x <= y iff f . x <= f . y ) ) ) by A4, WAYBEL_0:66;

now

Re is reflexive by A3, Def3;
hence Se is reflexive by A1, WAYBEL20:15; :: thesis: Se is transitive
Re is transitive by A3, Def3;
hence Se is transitive by A1, WAYBEL20:16; :: thesis: verum

end;

hence A6: S is quasi_ordered by Def3; :: thesis: S is Dickson

now

let t be sequence of Se; :: thesis: ex i, j being Element of NAT st
( i < j & t . i <= t . j )
reconsider fi = f " as Function of the carrier of Se,the carrier of Re by A5, FUNCT_2:31;
deffunc H₁( Element of NAT ) -> Element of the carrier of Re = fi . (t . $1);
consider sr being Function of NAT ,the carrier of Re such that
A7: for x being Element of NAT holds sr . x = H₁(x) from FUNCT_2:sch 4();
reconsider sr = sr as sequence of Re ;
consider i, j being Element of NAT such that
A8: i < j and
A9: sr . i <= sr . j by A2, A3, Th30;
take i = i; :: thesis: ex j being Element of NAT st
( i < j & t . i <= t . j )
take j = j; :: thesis: ( i < j & t . i <= t . j )
thus i < j by A8; :: thesis: t . i <= t . j
A10: f . (sr . i) = f . ((f " ) . (t . i)) by A7
.= t . i by A5, FUNCT_1:57 ;
f . (sr . j) = f . ((f " ) . (t . j)) by A7
.= t . j by A5, FUNCT_1:57 ;
hence t . i <= t . j by A4, A9, A10, WAYBEL_0:66; :: thesis: verum

end;

then for N being non empty Subset of Se holds
( min-classes N is finite & not min-classes N is empty ) by A6, Th32;
hence S is Dickson by A6, Th33; :: thesis: verum

end;

suppose A11: ( R is empty or S is empty ) ; :: thesis: ( S is quasi_ordered & S is Dickson )

A12: now

per cases ( R is empty or S is empty ) by A11;

suppose A13: R is empty ; :: thesis: S is empty

consider f being Function of R,S such that
A14: f is isomorphic by A1, WAYBEL_1:def 8;
thus S is empty by A13, A14, WAYBEL_0:def 38; :: thesis: verum

end;

suppose S is empty ; :: thesis: S is empty

hence S is empty ; :: thesis: verum

end;

end;

end;

now

for x being set st x in the carrier of S holds
[x,x] in the InternalRel of S by A12;
then the InternalRel of S is_reflexive_in the carrier of S by RELAT_2:def 1;
hence S is reflexive by ORDERS_2:def 4; :: thesis: S is transitive
for x, y, z being set st x in the carrier of S & y in the carrier of S & z in the carrier of S & [x,y] in the InternalRel of S & [y,z] in the InternalRel of S holds
[x,z] in the InternalRel of S by A12;
then the InternalRel of S is_transitive_in the carrier of S by RELAT_2:def 8;
hence S is transitive by ORDERS_2:def 5; :: thesis: verum

end;

hence S is quasi_ordered by Def3; :: thesis: S is Dickson
thus S is Dickson by A12, Th37; :: thesis: verum

end;

end;