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;

hereby :: thesis: ( ( for f being sequence of R holds not f is descending ) implies 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;

assume A9: for f being sequence of R holds not f is descending ; :: thesis: R is well_founded
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₁( 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₁(n,f . n) from NAT_1:sch 11();
defpred S₁[ Nat] means f . $1 in Y;

A16: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[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₁[n + 1] by A17, XBOOLE_0:def 4; :: thesis: verum

end;

A18: S₁[ 0 ] by A11, A14;
A19: for n being Nat holds S₁[n] from NAT_1:sch 2(A18, A16);
rng f c= the carrier of R

proof

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;

then reconsider f = f as sequence of R by A13, FUNCT_2:2;

now :: thesis: for n being Nat holds
( 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;

then f is descending ;
hence contradiction by A9; :: thesis: verum