let R, S be non empty RelStr ; 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; ( 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 ) )
; 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 for f being sequence of (R \~) holds not f is descending assume
ex
f being
sequence of
(R \~) st
f is
descending
;
contradictionthen consider f being
sequence of
(R \~) such that A6:
f is
descending
;
reconsider f9 =
f as
sequence of
R ;
deffunc H1(
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 = H1(
k)
from FUNCT_2:sch 4();
reconsider g =
g9 as
sequence of
(S \~) ;
now for n being Nat holds
( g . (n + 1) <> g . n & [(g . (n + 1)),(g . n)] in the InternalRel of (S \~) )let n be
Nat;
( 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 not g . (n + 1) = g . nend; hence
g . (n + 1) <> g . n
;
[(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;
verum end; then
g is
descending
by WELLFND1:def 6;
hence
contradiction
by A3, WELLFND1:14;
verum end;
hence
R \~ is well_founded
by WELLFND1:14; verum