set ir = the InternalRel of OrderedNAT ;
now given f being
sequence of
OrderedNAT such that A13:
f is
descending
;
:: thesis: contradictionA14:
dom f = NAT
by FUNCT_2:def 1;
reconsider rf =
rng f as non
empty Subset of
NAT ;
set m =
min rf;
min rf in rng f
by XXREAL_2:def 7;
then consider d being
set such that A15:
(
d in dom f &
min rf = f . d )
by FUNCT_1:def 5;
reconsider d =
d as
Element of
NAT by A15;
A16:
(
f . (d + 1) <> f . d &
[(f . (d + 1)),(f . d)] in the
InternalRel of
OrderedNAT )
by A13, WELLFND1:def 7;
then consider x,
y being
Element of
NAT such that A17:
[(f . (d + 1)),(f . d)] = [x,y]
and A18:
x <= y
;
reconsider fd1 =
f . (d + 1),
fd =
f . d as
Element of
NAT ;
(
f . (d + 1) = x &
f . d = y )
by A17, ZFMISC_1:33;
then A19:
fd1 < fd
by A16, A18, XXREAL_0:1;
f . (d + 1) in rf
by A14, FUNCT_1:12;
hence
contradiction
by A15, A19, XXREAL_2:def 7;
:: thesis: verum end;
hence
OrderedNAT is well_founded
by WELLFND1:15; :: thesis: verum