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 ;
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 ;
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 H1( 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) = H1(n,f . n) from NAT_1:sch 11();
defpred S1[ Nat] means f . \$1 in Y;
A16: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; :: thesis: S1[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 S1[n + 1] by ; :: thesis: verum
end;
A18: S1[ 0 ] by ;
A19: for n being Nat holds S1[n] from 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 ;
f . n in Y by A19;
hence y in the carrier of R by ; :: thesis: verum
end;
then reconsider f = f as sequence of R by ;
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 ;
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 ;
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