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;

now :: thesis: for f being sequence of (R \~) holds not f is descending

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 f9 = f as sequence of R ;
deffunc H₁( Element of NAT ) -> Element of the carrier of S = m . (f9 . $1);
consider g9 being sequence of the carrier of S such that
A7: for k being Element of NAT holds g9 . k = H₁(k) from FUNCT_2:sch 4();
reconsider g = g9 as sequence of (S \~) ;

now :: thesis: for n being Nat holds
( g . (n + 1) <> g . n & [(g . (n + 1)),(g . n)] in the InternalRel of (S \~) )

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

A12: now :: thesis: not g . (n + 1) = g . n

assume g . (n + 1) = g . n ; :: thesis: contradiction
then m . (f . (n + 1)) = m . (f . n) by A7, A11;
then [(f9 . (n + 1)),(f9 . 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;
A14: g9 . (n + 1) = m . fn1 by A7;
g9 . n1 = m . fn by A7;
then g9 . (n + 1) <= g9 . n by A4, A13, A14;
then A15: [(g . (n + 1)),(g . n)] in the InternalRel of S ;
then not [(g . n),(g . (n + 1))] in the InternalRel of S by A5, A12;
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 A15, XBOOLE_0:def 5; :: thesis: verum

end;

then g is descending by WELLFND1:def 6;
hence contradiction by A3, WELLFND1:14; :: thesis: verum

end;

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