let R, S be non empty RelStr ; :: thesis: for m being Function of R,S st R is quasi_ordered & S is antisymmetric & S \~ is well_founded & ( for a, b being Element of R holds
( ( a <= b implies m . a <= m . b ) & ( m . a = m . b implies [a,b] in EqRel R ) ) ) holds
R \~ is well_founded
let m be Function of R,S; :: thesis: ( R is quasi_ordered & S is antisymmetric & S \~ is well_founded & ( for a, b being Element of R holds
( ( a <= b implies m . a <= m . b ) & ( m . a = m . b implies [a,b] in EqRel R ) ) ) implies R \~ is well_founded )
assume that
A1: R is quasi_ordered and
A2: S is antisymmetric and
A3: S \~ is well_founded and
A4: for a, b being Element of R holds
( ( a <= b implies m . a <= m . b ) & ( m . a = m . b implies [a,b] in EqRel R ) ) ; :: thesis: R \~ is well_founded
set IR = the InternalRel of R;
set IS = the InternalRel of S;
A5: the InternalRel of S is_antisymmetric_in the carrier of S by A2, ORDERS_2:def 6;

now

assume ex f being sequence of (R \~ ) st f is descending ; :: thesis: contradiction
then consider f being sequence of (R \~ ) such that
A6: f is descending ;
reconsider f' = f as sequence of R ;
deffunc H₁( Element of NAT ) -> Element of the carrier of S = m . (f' . $1);
consider g' being Function of NAT ,the carrier of S such that
A7: for k being Element of NAT holds g' . k = H₁(k) from FUNCT_2:sch 4();
reconsider g = g' as sequence of (S \~ ) ;

now

let n be Element of NAT ; :: thesis: ( g . (n + 1) <> g . n & [(g . (n + 1)),(g . n)] in the InternalRel of (S \~ ) )
A8: [(f . (n + 1)),(f . n)] in the InternalRel of (R \~ ) by A6, WELLFND1:def 7;
A9: [(f . (n + 1)),(f . n)] in the InternalRel of R \ (the InternalRel of R ~ ) by A6, WELLFND1:def 7;
A10: ( not [(f . (n + 1)),(f . n)] in the InternalRel of R ~ & [(f . (n + 1)),(f . n)] in the InternalRel of R ) by A8, XBOOLE_0:def 5;
A11: g . n = m . (f . n) by A7;

A12: now

assume g . (n + 1) = g . n ; :: thesis: contradiction
then m . (f . (n + 1)) = m . (f . n) by A7, A11;
then [(f' . (n + 1)),(f' . n)] in EqRel R by A4;
then [(f . (n + 1)),(f . n)] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
hence contradiction by A10, XBOOLE_0:def 4; :: thesis: verum

end;

hence g . (n + 1) <> g . n ; :: thesis: [(g . (n + 1)),(g . n)] in the InternalRel of (S \~ )
reconsider fn1 = f . (n + 1) as Element of R ;
reconsider fn = f . n as Element of R ;
A13: fn1 <= fn by A9, ORDERS_2:def 9;
( g' . (n + 1) = m . fn1 & g' . n = m . fn ) by A7;
then g' . (n + 1) <= g' . n by A4, A13;
then A14: [(g . (n + 1)),(g . n)] in the InternalRel of S by ORDERS_2:def 9;
then not [(g . n),(g . (n + 1))] in the InternalRel of S by A5, A12, RELAT_2:def 4;
then not [(g . (n + 1)),(g . n)] in the InternalRel of S ~ by RELAT_1:def 7;
hence [(g . (n + 1)),(g . n)] in the InternalRel of (S \~ ) by A14, XBOOLE_0:def 5; :: thesis: verum

end;

then g is descending by WELLFND1:def 7;
hence contradiction by A3, WELLFND1:15; :: thesis: verum

end;

hence R \~ is well_founded by WELLFND1:15; :: thesis: verum