set ir = the InternalRel of OrderedNAT;
now for f being sequence of OrderedNAT holds not f is descending given f being
sequence of
OrderedNAT such that A16:
f is
descending
;
contradictionA17:
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
object such that A18:
d in dom f
and A19:
min rf = f . d
by FUNCT_1:def 3;
reconsider d =
d as
Element of
NAT by A18;
A20:
f . (d + 1) <> f . d
by A16, WELLFND1:def 6;
[(f . (d + 1)),(f . d)] in the
InternalRel of
OrderedNAT
by A16, WELLFND1:def 6;
then consider x,
y being
Element of
NAT such that A21:
[(f . (d + 1)),(f . d)] = [x,y]
and A22:
x <= y
;
reconsider fd1 =
f . (d + 1),
fd =
f . d as
Element of
NAT ;
A23:
f . (d + 1) = x
by A21, XTUPLE_0:1;
f . d = y
by A21, XTUPLE_0:1;
then A24:
fd1 < fd
by A20, A22, A23, XXREAL_0:1;
f . (d + 1) in rf
by A17, FUNCT_1:3;
hence
contradiction
by A19, A24, XXREAL_2:def 7;
verum end;
hence
OrderedNAT is well_founded
by WELLFND1:14; verum