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 by Def2;
given f being sequence of R such that A2: f is descending ; :: thesis: contradiction
A3: ( dom f = NAT & rng f c= the carrier of R ) by FUNCT_2:def 1;
then rng f <> {} by RELAT_1:65;
then consider a being set such that
A4: ( a in rng f & the InternalRel of R -Seg a misses rng f ) by A1, WELLORD1:def 3;
consider n being set such that
A5: ( n in dom f & a = f . n ) by A4, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A5;
( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) by A2, Def7;
then A6: f . (n + 1) in the InternalRel of R -Seg (f . n) by WELLORD1:def 1;
f . (n + 1) in rng f by A3, FUNCT_1:def 5;
hence contradiction by A4, A5, A6, XBOOLE_0:3; :: thesis: verum

end;

assume A7: 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 by Def2;
then consider Y being set such that
A8: ( Y c= the carrier of R & Y <> {} ) and
A9: for a being set holds
( not a in Y or the InternalRel of R -Seg a meets Y ) by WELLORD1:def 3;
deffunc H₁( set , set ) -> Element of (the InternalRel of R -Seg $2) /\ Y = choose ((the InternalRel of R -Seg $2) /\ Y);
consider f being Function such that
A10: dom f = NAT and
A11: f . 0 = choose Y and
A12: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 11();
defpred S₁[ Element of NAT ] means f . $1 in Y;
A13: S₁[ 0 ] by A8, A11;

A14: now

let n be Element of 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 A9;
then A15: (the InternalRel of R -Seg (f . n)) /\ Y <> {} by XBOOLE_0:def 7;
f . (n + 1) = choose ((the InternalRel of R -Seg (f . n)) /\ Y) by A12;
hence S₁[n + 1] by A15, XBOOLE_0:def 4; :: thesis: verum

end;

A16: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A13, A14);
rng f c= the carrier of R

proof

let y be set ; :: 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 set such that
A17: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A10, A17;
f . n in Y by A16;
hence y in the carrier of R by A8, A17; :: thesis: verum

end;

then reconsider f = f as sequence of R by A10, FUNCT_2:4;

now

let n be Element of 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 A9, A16;
then A18: (the InternalRel of R -Seg (f . n)) /\ Y <> {} by XBOOLE_0:def 7;
f . (n + 1) = choose ((the InternalRel of R -Seg (f . n)) /\ Y) by A12;
then f . (n + 1) in the InternalRel of R -Seg (f . n) by A18, XBOOLE_0:def 4;
hence ( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) by WELLORD1:def 1; :: thesis: verum

end;

then f is descending by Def7;
hence contradiction by A7; :: thesis: verum