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;

( ( 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

hence
R \~ is well_founded
by WELLFND1:14; :: thesis: verumassume
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_{1}( 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_{1}(k)
from FUNCT_2:sch 4();

reconsider g = g9 as sequence of (S \~) ;

hence contradiction by A3, WELLFND1:14; :: thesis: verum

end;then consider f being sequence of (R \~) such that

A6: f is descending ;

reconsider f9 = f as sequence of R ;

deffunc H

consider g9 being sequence of the carrier of S such that

A7: for k being Element of NAT holds g9 . k = H

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 \~) )

then
g is descending
by WELLFND1:def 6;( 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;

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;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

hence
g . (n + 1) <> g . n
; :: thesis: [(g . (n + 1)),(g . n)] in the InternalRel of (S \~)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;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

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

hence contradiction by A3, WELLFND1:14; :: thesis: verum