let R be non empty RelStr ; :: thesis: ( R is well_founded iff for f being sequence of R holds not f is descending )

set c = the carrier of R;

set r = the InternalRel of R;

assume not R is well_founded ; :: thesis: contradiction

then not the InternalRel of R is_well_founded_in the carrier of R ;

then consider Y being set such that

A10: Y c= the carrier of R and

A11: Y <> {} and

A12: for a being object holds

( not a in Y or the InternalRel of R -Seg a meets Y ) ;

deffunc H_{1}( set , set ) -> Element of ( the InternalRel of R -Seg $2) /\ Y = the Element of ( the InternalRel of R -Seg $2) /\ Y;

consider f being Function such that

A13: dom f = NAT and

A14: f . 0 = the Element of Y and

A15: for n being Nat holds f . (n + 1) = H_{1}(n,f . n)
from NAT_1:sch 11();

defpred S_{1}[ Nat] means f . $1 in Y;

_{1}[ 0 ]
by A11, A14;

A19: for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A18, A16);

rng f c= the carrier of R

hence contradiction by A9; :: thesis: verum

set c = the carrier of R;

set r = the InternalRel of R;

hereby :: thesis: ( ( for f being sequence of R holds not f is descending ) implies R is well_founded )

assume A9:
for f being sequence of R holds not f is descending
; :: thesis: R is well_founded assume
R is well_founded
; :: thesis: for f being sequence of R holds not f is descending

then A1: the InternalRel of R is_well_founded_in the carrier of R ;

given f being sequence of R such that A2: f is descending ; :: thesis: contradiction

A3: dom f = NAT by FUNCT_2:def 1;

then rng f <> {} by RELAT_1:42;

then consider a being object such that

A4: a in rng f and

A5: the InternalRel of R -Seg a misses rng f by A1;

consider n being object such that

A6: n in dom f and

A7: a = f . n by A4, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A6;

( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) by A2;

then A8: f . (n + 1) in the InternalRel of R -Seg (f . n) by WELLORD1:1;

f . (n + 1) in rng f by A3, FUNCT_1:def 3;

hence contradiction by A5, A7, A8, XBOOLE_0:3; :: thesis: verum

end;then A1: the InternalRel of R is_well_founded_in the carrier of R ;

given f being sequence of R such that A2: f is descending ; :: thesis: contradiction

A3: dom f = NAT by FUNCT_2:def 1;

then rng f <> {} by RELAT_1:42;

then consider a being object such that

A4: a in rng f and

A5: the InternalRel of R -Seg a misses rng f by A1;

consider n being object such that

A6: n in dom f and

A7: a = f . n by A4, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A6;

( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) by A2;

then A8: f . (n + 1) in the InternalRel of R -Seg (f . n) by WELLORD1:1;

f . (n + 1) in rng f by A3, FUNCT_1:def 3;

hence contradiction by A5, A7, A8, XBOOLE_0:3; :: thesis: verum

assume not R is well_founded ; :: thesis: contradiction

then not the InternalRel of R is_well_founded_in the carrier of R ;

then consider Y being set such that

A10: Y c= the carrier of R and

A11: Y <> {} and

A12: for a being object holds

( not a in Y or the InternalRel of R -Seg a meets Y ) ;

deffunc H

consider f being Function such that

A13: dom f = NAT and

A14: f . 0 = the Element of Y and

A15: for n being Nat holds f . (n + 1) = H

defpred S

A16: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A18:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume S_{1}[n]
; :: thesis: S_{1}[n + 1]

then the InternalRel of R -Seg (f . n) meets Y by A12;

then A17: ( the InternalRel of R -Seg (f . n)) /\ Y <> {} ;

f . (n + 1) = the Element of ( the InternalRel of R -Seg (f . n)) /\ Y by A15;

hence S_{1}[n + 1]
by A17, XBOOLE_0:def 4; :: thesis: verum

end;assume S

then the InternalRel of R -Seg (f . n) meets Y by A12;

then A17: ( the InternalRel of R -Seg (f . n)) /\ Y <> {} ;

f . (n + 1) = the Element of ( the InternalRel of R -Seg (f . n)) /\ Y by A15;

hence S

A19: for n being Nat holds S

rng f c= the carrier of R

proof

then reconsider f = f as sequence of R by A13, FUNCT_2:2;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of R )

assume y in rng f ; :: thesis: y in the carrier of R

then consider x being object such that

A20: x in dom f and

A21: y = f . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A13, A20;

f . n in Y by A19;

hence y in the carrier of R by A10, A21; :: thesis: verum

end;assume y in rng f ; :: thesis: y in the carrier of R

then consider x being object such that

A20: x in dom f and

A21: y = f . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A13, A20;

f . n in Y by A19;

hence y in the carrier of R by A10, A21; :: thesis: verum

now :: thesis: for n being Nat holds

( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R )

then
f is descending
;( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R )

let n be Nat; :: thesis: ( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R )

the InternalRel of R -Seg (f . n) meets Y by A12, A19;

then A22: ( the InternalRel of R -Seg (f . n)) /\ Y <> {} ;

f . (n + 1) = the Element of ( the InternalRel of R -Seg (f . n)) /\ Y by A15;

then f . (n + 1) in the InternalRel of R -Seg (f . n) by A22, XBOOLE_0:def 4;

hence ( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) by WELLORD1:1; :: thesis: verum

end;the InternalRel of R -Seg (f . n) meets Y by A12, A19;

then A22: ( the InternalRel of R -Seg (f . n)) /\ Y <> {} ;

f . (n + 1) = the Element of ( the InternalRel of R -Seg (f . n)) /\ Y by A15;

then f . (n + 1) in the InternalRel of R -Seg (f . n) by A22, XBOOLE_0:def 4;

hence ( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) by WELLORD1:1; :: thesis: verum

hence contradiction by A9; :: thesis: verum