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 by A4, WAYBEL_0:66;
A6: rng f = the carrier of Se by A4, WAYBEL_0:66;
A7: Re is reflexive by A3, Def3;
A8: Re is transitive by A3, Def3;
A9: Se is reflexive by A1, A7, WAYBEL20:15;
Se is transitive by A1, A8, WAYBEL20:16;
hence A10: S is quasi_ordered by A9, 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, A6, FUNCT_2:25;
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
A11: 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
A12: i < j and
A13: sr . i <= sr . j by A2, 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 A12; :: thesis: t . i <= t . j
A14: f . (sr . i) = f . ((f ") . (t . i)) by A11
.= t . i by A5, A6, FUNCT_1:35 ;
f . (sr . j) = f . ((f ") . (t . j)) by A11
.= t . j by A5, A6, FUNCT_1:35 ;
hence t . i <= t . j by A4, A13, A14, 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 A10, Th32;
hence S is Dickson by A10, Th33; :: thesis: verum

end;

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

A16: now

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

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

ex f being Function of R,S st f is isomorphic by A1, WAYBEL_1:def 8;
hence S is empty by A17, WAYBEL_0:def 38; :: thesis: verum

end;

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

hence S is empty ; :: thesis: verum

end;

end;

end;

then for x being set st x in the carrier of S holds
[x,x] in the InternalRel of S ;
then A18: the InternalRel of S is_reflexive_in the carrier of S by RELAT_2:def 1;
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 A16;
then A19: the InternalRel of S is_transitive_in the carrier of S by RELAT_2:def 8;
A20: S is reflexive by A18, ORDERS_2:def 2;
S is transitive by A19, ORDERS_2:def 3;
hence S is quasi_ordered by A20, Def3; :: thesis: S is Dickson
thus S is Dickson by A16, Th37; :: thesis: verum

end;

end;