:: WELLFND1 semantic presentation

begin

theorem Th1: :: WELLFND1:1
for X being functional set st ( for f, g being Function st f in X & g in X holds
f tolerates g ) holds
union X is Function
proof
let X be functional set ; ::_thesis: ( ( for f, g being Function st f in X & g in X holds
f tolerates g ) implies union X is Function )
assume A1: for f, g being Function st f in X & g in X holds
f tolerates g ; ::_thesis: union X is Function
A2: union X is Function-like
proof
let x, y1, y2 be set ; :: according to FUNCT_1:def_1 ::_thesis: ( not [x,y1] in union X or not [x,y2] in union X or y1 = y2 )
assume that
A3: [x,y1] in union X and
A4: [x,y2] in union X and
A5: y1 <> y2 ; ::_thesis: contradiction
consider gx being set  such that
A6: [x,y2] in gx and
A7: gx in X by A4, TARSKI:def_4;
consider fx being set  such that
A8: [x,y1] in fx and
A9: fx in X by A3, TARSKI:def_4;
reconsider fx = fx, gx = gx as Function by A9, A7;
 fx tolerates gx by A1, A9, A7;
then  ex h being Function st
( fx c= h & gx c= h ) by PARTFUN1:52;
hence  contradiction by A5, A8, A6, FUNCT_1:def_1; ::_thesis: verum
end;
 union X is Relation-like
proof
let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( not x in union X or ex b1, b2 being set st x = [b1,b2] )
assume  x in union X ; ::_thesis: ex b1, b2 being set st x = [b1,b2]
then  ex ux being set st
( x in ux & ux in X ) by TARSKI:def_4;
hence  ex b1, b2 being set st x = [b1,b2] by RELAT_1:def_1; ::_thesis: verum
end;
hence  union X is Function by A2; ::_thesis: verum
end;

scheme :: WELLFND1:sch 1
PFSeparation{ F1() ->  set , F2() ->  set , P1[ set ] } :
 ex PFS being Subset of (PFuncs (F1(),F2())) st
for pfs being PartFunc of F1(),F2() holds
( pfs in PFS iff P1[pfs] )
proof
consider fs being Subset of (PFuncs (F1(),F2())) such that
A1: for f being set holds
( f in fs iff ( f in PFuncs (F1(),F2()) & P1[f] ) ) from SUBSET_1:sch_1();
take  fs ; ::_thesis: for pfs being PartFunc of F1(),F2() holds
( pfs in fs iff P1[pfs] )
let pfs be PartFunc of F1(),F2(); ::_thesis: ( pfs in fs iff P1[pfs] )
 pfs in PFuncs (F1(),F2()) by PARTFUN1:45;
hence  ( pfs in fs iff P1[pfs] ) by A1; ::_thesis: verum
end;

registration
let X be set ;
cluster nextcard X ->  non empty ;
coherence
 not nextcard X is empty by CARD_1:def_3;
end;

registration
cluster non empty epsilon-transitive epsilon-connected ordinal non finite cardinal regular for set ;
existence
 ex b1 being Aleph st b1 is regular by CARD_5:30;
end;

theorem Th2: :: WELLFND1:2
for M being regular Aleph
for X being set st X c= M & card X in M holds
sup X in M
proof
let M be regular Aleph; ::_thesis: for X being set st X c= M & card X in M holds
sup X in M
 cf M = M by CARD_5:def_3;
hence  for X being set st X c= M & card X in M holds
sup X in M by CARD_5:26; ::_thesis: verum
end;

theorem Th3: :: WELLFND1:3
for R being RelStr
for x being set holds the InternalRel of R -Seg x c= the carrier of R
proof
let R be RelStr ; ::_thesis: for x being set holds the InternalRel of R -Seg x c= the carrier of R
let x be set ; ::_thesis: the InternalRel of R -Seg x c= the carrier of R
set r = the InternalRel of R;
set c = the carrier of R;
 ( the InternalRel of R -Seg x c= field the InternalRel of R & field the InternalRel of R c= the carrier of R \/ the carrier of R ) by RELSET_1:8, WELLORD1:9;
hence  the InternalRel of R -Seg x c= the carrier of R by XBOOLE_1:1; ::_thesis: verum
end;

definition
let R be RelStr ;
let X be Subset of R;
redefine attr X is lower  means :Def1: :: WELLFND1:def 1
 for x, y being set st x in X & [y,x] in the InternalRel of R holds
y in X;
compatibility
 ( X is lower iff for x, y being set st x in X & [y,x] in the InternalRel of R holds
y in X )
proof
hereby  ::_thesis: ( ( for x, y being set st x in X & [y,x] in the InternalRel of R holds
y in X ) implies X is lower )
assume A1: X is lower ; ::_thesis: for x, y being set st x in X & [y,x] in the InternalRel of R holds
y in X
let x, y be set ; ::_thesis: ( x in X & [y,x] in the InternalRel of R implies y in X )
assume that
A2: x in X and
A3: [y,x] in the InternalRel of R ; ::_thesis: y in X
reconsider x9 = x, y9 = y as Element of R by A3, ZFMISC_1:87;
 y9 <= x9 by A3, ORDERS_2:def_5;
hence  y in X by A1, A2, WAYBEL_0:def_19; ::_thesis: verum
end;
assume A4: for x, y being set st x in X & [y,x] in the InternalRel of R holds
y in X ; ::_thesis: X is lower
let x, y be Element of R; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in X or not y <= x or y in X )
assume A5: x in X ; ::_thesis: ( not y <= x or y in X )
assume  y <= x ; ::_thesis: y in X
then  [y,x] in the InternalRel of R by ORDERS_2:def_5;
hence  y in X by A4, A5; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines lower WELLFND1:def_1_:_
 for R being RelStr
for X being Subset of R holds
( X is lower iff for x, y being set st x in X & [y,x] in the InternalRel of R holds
y in X );

theorem Th4: :: WELLFND1:4
for R being RelStr
for X being Subset of R
for x being set st X is lower & x in X holds
the InternalRel of R -Seg x c= X
proof
let R be RelStr ; ::_thesis: for X being Subset of R
for x being set st X is lower & x in X holds
the InternalRel of R -Seg x c= X
let X be Subset of R; ::_thesis: for x being set st X is lower & x in X holds
the InternalRel of R -Seg x c= X
let x be set ; ::_thesis: ( X is lower & x in X implies the InternalRel of R -Seg x c= X )
assume A1: ( X is lower & x in X ) ; ::_thesis: the InternalRel of R -Seg x c= X
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the InternalRel of R -Seg x or z in X )
assume  z in the InternalRel of R -Seg x ; ::_thesis: z in X
then  [z,x] in the InternalRel of R by WELLORD1:1;
hence  z in X by A1, Def1; ::_thesis: verum
end;

theorem Th5: :: WELLFND1:5
for R being RelStr
for X being lower Subset of R
for Y being Subset of R
for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds
Y is lower
proof
let R be RelStr ; ::_thesis: for X being lower Subset of R
for Y being Subset of R
for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds
Y is lower
let X be lower Subset of R; ::_thesis: for Y being Subset of R
for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds
Y is lower
let Y be Subset of R; ::_thesis: for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds
Y is lower
let x be set ; ::_thesis: ( Y = X \/ {x} & the InternalRel of R -Seg x c= X implies Y is lower )
set r = the InternalRel of R;
assume that
A1: Y = X \/ {x} and
A2: the InternalRel of R -Seg x c= X ; ::_thesis: Y is lower
let z, y be set ; :: according to WELLFND1:def_1 ::_thesis: ( z in Y & [y,z] in the InternalRel of R implies y in Y )
assume that
A3: z in Y and
A4: [y,z] in the InternalRel of R ; ::_thesis: y in Y
percases ( z in X or ( z in {x} & y = z ) or ( z in {x} & y <> z ) ) by A1, A3, XBOOLE_0:def_3;
suppose z in X ; ::_thesis: y in Y
then  y in X by A4, Def1;
hence  y in Y by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( z in {x} & y = z ) ; ::_thesis: y in Y
hence  y in Y by A3; ::_thesis: verum
end;
supposeA5: ( z in {x} & y <> z ) ; ::_thesis: y in Y
then  z = x by TARSKI:def_1;
then  y in the InternalRel of R -Seg x by A4, A5, WELLORD1:1;
hence  y in Y by A1, A2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;

begin

definition
let R be RelStr ;
attrR is well_founded  means :Def2: :: WELLFND1:def 2
 the InternalRel of R is_well_founded_in the carrier of R;
end;

:: deftheorem Def2 defines well_founded WELLFND1:def_2_:_
 for R being RelStr holds
( R is well_founded iff the InternalRel of R is_well_founded_in the carrier of R );

registration
cluster non empty well_founded for RelStr ;
existence
 ex b1 being RelStr st
( not b1 is empty & b1 is well_founded )
proof
reconsider er = {} as Relation of {{}} by RELSET_1:12;
take R = RelStr(# {{}},er #); ::_thesis: ( not R is empty & R is well_founded )
thus  not R is empty ; ::_thesis: R is well_founded
let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_2 ::_thesis: ( not Y c= the carrier of R or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )
assume A1: ( Y c= the carrier of R & Y <> {} ) ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )
take e = {} ; ::_thesis: ( e in Y & the InternalRel of R -Seg e misses Y )
 Y = {{}} by A1, ZFMISC_1:33;
hence  e in Y by TARSKI:def_1; ::_thesis: the InternalRel of R -Seg e misses Y
assume  ( the InternalRel of R -Seg e) /\ Y <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being set  such that
A2: x in ( the InternalRel of R -Seg e) /\ Y by XBOOLE_0:def_1;
 x in the InternalRel of R -Seg e by A2, XBOOLE_0:def_4;
hence  contradiction by WELLORD1:1; ::_thesis: verum
end;
end;

definition
let R be RelStr ;
let X be Subset of R;
attrX is well_founded  means :Def3: :: WELLFND1:def 3
 the InternalRel of R is_well_founded_in X;
end;

:: deftheorem Def3 defines well_founded WELLFND1:def_3_:_
 for R being RelStr
for X being Subset of R holds
( X is well_founded iff the InternalRel of R is_well_founded_in X );

registration
let R be RelStr ;
cluster well_founded for Element of bool the carrier of R;
existence
 ex b1 being Subset of R st b1 is well_founded
proof
reconsider e = {} as Subset of R by XBOOLE_1:2;
take  e ; ::_thesis: e is well_founded
let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_3 ::_thesis: ( not Y c= e or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )
assume  ( Y c= e & Y <> {} ) ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )
hence  ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) ; ::_thesis: verum
end;
end;

definition
let R be RelStr ;
func well_founded-Part R ->  Subset of R means :Def4: :: WELLFND1:def 4
it = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  ;
existence
 ex b1 being Subset of R st b1 = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }
proof
set IT =  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  ;
  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  c= bool the carrier of R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  or x in bool the carrier of R )
assume  x in  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  ; ::_thesis: x in bool the carrier of R
then  ex S being Subset of R st
( x = S & S is well_founded & S is lower ) ;
hence  x in bool the carrier of R ; ::_thesis: verum
end;
then reconsider IT =  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  as Subset-Family of R ;
 union IT is Subset of R ;
hence  ex b1 being Subset of R st b1 = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of R st b1 = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  & b2 = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  holds
b1 = b2 ;
end;

:: deftheorem Def4 defines well_founded-Part WELLFND1:def_4_:_
 for R being RelStr
for b2 being Subset of R holds
( b2 = well_founded-Part R iff b2 = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  );

registration
let R be RelStr ;
cluster well_founded-Part R ->  lower well_founded ;
coherence
 ( well_founded-Part R is lower & well_founded-Part R is well_founded )
proof
set wfp = well_founded-Part R;
set r = the InternalRel of R;
set IT =  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  ;
A1: well_founded-Part R = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  by Def4;
hereby  :: according to WELLFND1:def_1 ::_thesis: well_founded-Part R is well_founded
let x, y be set ; ::_thesis: ( x in well_founded-Part R & [y,x] in the InternalRel of R implies y in well_founded-Part R )
assume that
A2: x in well_founded-Part R and
A3: [y,x] in the InternalRel of R ; ::_thesis: y in well_founded-Part R
consider Y being set  such that
A4: x in Y and
A5: Y in  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  by A1, A2, TARSKI:def_4;
consider S being Subset of R such that
A6: Y = S and
A7: ( S is well_founded & S is lower ) by A5;
 y in S by A3, A4, A6, A7, Def1;
hence  y in well_founded-Part R by A1, A5, A6, TARSKI:def_4; ::_thesis: verum
end;
let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_3 ::_thesis: ( not Y c= well_founded-Part R or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )
assume that
A8: Y c= well_founded-Part R and
A9: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )
consider y being set  such that
A10: y in Y by A9, XBOOLE_0:def_1;
consider YY being set  such that
A11: y in YY and
A12: YY in  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  by A1, A8, A10, TARSKI:def_4;
consider S being Subset of R such that
A13: YY = S and
A14: ( S is well_founded & S is lower ) by A12;
set YS = Y /\ S;
A15: the InternalRel of R is_well_founded_in S by A14, Def3;
 ( Y /\ S c= S & Y /\ S <> {} ) by A10, A11, A13, XBOOLE_0:def_4, XBOOLE_1:17;
then consider a being set  such that
A16: a in Y /\ S and
A17: the InternalRel of R -Seg a misses Y /\ S by A15, WELLORD1:def_3;
A18: a in Y by A16, XBOOLE_0:def_4;
 a in S by A16, XBOOLE_0:def_4;
then A19: ( the InternalRel of R -Seg a) /\ Y = (( the InternalRel of R -Seg a) /\ S) /\ Y by A14, Th4, XBOOLE_1:28
.= ( the InternalRel of R -Seg a) /\ (Y /\ S) by XBOOLE_1:16 ;
 ( the InternalRel of R -Seg a) /\ (Y /\ S) = {} by A17, XBOOLE_0:def_7;
then  the InternalRel of R -Seg a misses Y by A19, XBOOLE_0:def_7;
hence  ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) by A18; ::_thesis: verum
end;
end;

theorem Th6: :: WELLFND1:6
for R being non empty RelStr
for x being Element of R holds {x} is well_founded Subset of R
proof
let R be non empty RelStr ; ::_thesis: for x being Element of R holds {x} is well_founded Subset of R
let x be Element of R; ::_thesis: {x} is well_founded Subset of R
set r = the InternalRel of R;
reconsider sx = {x} as Subset of R ;
 sx is well_founded
proof
let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_3 ::_thesis: ( not Y c= sx or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )
assume that
A1: Y c= sx and
A2: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )
take  x ; ::_thesis: ( x in Y & the InternalRel of R -Seg x misses Y )
 Y = sx by A1, A2, ZFMISC_1:33;
hence  x in Y by TARSKI:def_1; ::_thesis: the InternalRel of R -Seg x misses Y
assume  not the InternalRel of R -Seg x misses Y ; ::_thesis: contradiction
then consider a being set  such that
A3: a in ( the InternalRel of R -Seg x) /\ Y by XBOOLE_0:4;
 a in the InternalRel of R -Seg x by A3, XBOOLE_0:def_4;
then A4: a <> x by WELLORD1:1;
 a in Y by A3, XBOOLE_0:def_4;
hence  contradiction by A1, A4, TARSKI:def_1; ::_thesis: verum
end;
hence  {x} is well_founded Subset of R ; ::_thesis: verum
end;

theorem Th7: :: WELLFND1:7
for R being RelStr
for X, Y being well_founded Subset of R st X is lower holds
X \/ Y is well_founded Subset of R
proof
let R be RelStr ; ::_thesis: for X, Y being well_founded Subset of R st X is lower holds
X \/ Y is well_founded Subset of R
let X, Y be well_founded Subset of R; ::_thesis: ( X is lower implies X \/ Y is well_founded Subset of R )
set r = the InternalRel of R;
assume A1: X is lower ; ::_thesis: X \/ Y is well_founded Subset of R
reconsider XY = X \/ Y as Subset of R ;
A2: the InternalRel of R is_well_founded_in Y by Def3;
A3: the InternalRel of R is_well_founded_in X by Def3;
 XY is well_founded
proof
let Z be set ; :: according to WELLORD1:def_3,WELLFND1:def_3 ::_thesis: ( not Z c= XY or Z = {} or ex b1 being set st
( b1 in Z & the InternalRel of R -Seg b1 misses Z ) )
assume that
A4: Z c= XY and
A5: Z <> {} ; ::_thesis: ex b1 being set st
( b1 in Z & the InternalRel of R -Seg b1 misses Z )
set XZ = X /\ Z;
A6: X /\ Z c= X by XBOOLE_1:17;
percases ( X /\ Z = {} or X /\ Z <> {} ) ;
suppose X /\ Z = {} ; ::_thesis: ex b1 being set st
( b1 in Z & the InternalRel of R -Seg b1 misses Z )
then  X misses Z by XBOOLE_0:def_7;
then  Z c= Y by A4, XBOOLE_1:73;
hence  ex b1 being set st
( b1 in Z & the InternalRel of R -Seg b1 misses Z ) by A2, A5, WELLORD1:def_3; ::_thesis: verum
end;
suppose X /\ Z <> {} ; ::_thesis: ex b1 being set st
( b1 in Z & the InternalRel of R -Seg b1 misses Z )
then consider a being set  such that
A7: a in X /\ Z and
A8: the InternalRel of R -Seg a misses X /\ Z by A3, A6, WELLORD1:def_3;
A9: a in X by A7, XBOOLE_0:def_4;
take  a ; ::_thesis: ( a in Z & the InternalRel of R -Seg a misses Z )
thus  a in Z by A7, XBOOLE_0:def_4; ::_thesis: the InternalRel of R -Seg a misses Z
assume  ( the InternalRel of R -Seg a) /\ Z <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider b being set  such that
A10: b in ( the InternalRel of R -Seg a) /\ Z by XBOOLE_0:def_1;
A11: b in Z by A10, XBOOLE_0:def_4;
A12: b in the InternalRel of R -Seg a by A10, XBOOLE_0:def_4;
then  [b,a] in the InternalRel of R by WELLORD1:1;
then  b in X by A1, A9, Def1;
then  b in X /\ Z by A11, XBOOLE_0:def_4;
hence  contradiction by A8, A12, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence  X \/ Y is well_founded Subset of R ; ::_thesis: verum
end;

theorem Th8: :: WELLFND1:8
for R being RelStr holds
( R is well_founded iff well_founded-Part R = the carrier of R )
proof
let R be RelStr ; ::_thesis: ( R is well_founded iff well_founded-Part R = the carrier of R )
set r = the InternalRel of R;
set c = the carrier of R;
set wfp = well_founded-Part R;
set IT =  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  ;
 the carrier of R c= the carrier of R ;
then reconsider cs = the carrier of R as Subset of R ;
A1: well_founded-Part R = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  by Def4;
hereby  ::_thesis: ( well_founded-Part R = the carrier of R implies R is well_founded )
A2: cs is lower
proof
let x, y be set ; :: according to WELLFND1:def_1 ::_thesis: ( x in cs & [y,x] in the InternalRel of R implies y in cs )
thus  ( x in cs & [y,x] in the InternalRel of R implies y in cs ) by ZFMISC_1:87; ::_thesis: verum
end;
assume  R is well_founded ; ::_thesis: well_founded-Part R = the carrier of R
then  the InternalRel of R is_well_founded_in cs by Def2;
then  cs is well_founded by Def3;
then  cs in  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  by A2;
then  cs c= well_founded-Part R by A1, ZFMISC_1:74;
hence  well_founded-Part R = the carrier of R by XBOOLE_0:def_10; ::_thesis: verum
end;
assume A3: well_founded-Part R = the carrier of R ; ::_thesis: R is well_founded
let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_2 ::_thesis: ( not Y c= the carrier of R or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )
assume that
A4: Y c= the carrier of R and
A5: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )
consider y being set  such that
A6: y in Y by A5, XBOOLE_0:def_1;
consider YY being set  such that
A7: y in YY and
A8: YY in  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  by A1, A3, A4, A6, TARSKI:def_4;
consider S being Subset of R such that
A9: YY = S and
A10: ( S is well_founded & S is lower ) by A8;
set YS = Y /\ S;
A11: the InternalRel of R is_well_founded_in S by A10, Def3;
 ( Y /\ S c= S & Y /\ S <> {} ) by A6, A7, A9, XBOOLE_0:def_4, XBOOLE_1:17;
then consider a being set  such that
A12: a in Y /\ S and
A13: the InternalRel of R -Seg a misses Y /\ S by A11, WELLORD1:def_3;
A14: a in Y by A12, XBOOLE_0:def_4;
 a in S by A12, XBOOLE_0:def_4;
then A15: ( the InternalRel of R -Seg a) /\ Y = (( the InternalRel of R -Seg a) /\ S) /\ Y by A10, Th4, XBOOLE_1:28
.= ( the InternalRel of R -Seg a) /\ (Y /\ S) by XBOOLE_1:16 ;
 ( the InternalRel of R -Seg a) /\ (Y /\ S) = {} by A13, XBOOLE_0:def_7;
then  the InternalRel of R -Seg a misses Y by A15, XBOOLE_0:def_7;
hence  ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) by A14; ::_thesis: verum
end;

theorem Th9: :: WELLFND1:9
for R being non empty RelStr
for x being Element of R st the InternalRel of R -Seg x c= well_founded-Part R holds
x in well_founded-Part R
proof
let R be non empty RelStr ; ::_thesis: for x being Element of R st the InternalRel of R -Seg x c= well_founded-Part R holds
x in well_founded-Part R
let x be Element of R; ::_thesis: ( the InternalRel of R -Seg x c= well_founded-Part R implies x in well_founded-Part R )
set wfp = well_founded-Part R;
set IT =  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  ;
set xwfp = (well_founded-Part R) \/ {x};
A1: well_founded-Part R = union  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  by Def4;
 x in {x} by TARSKI:def_1;
then A2: x in (well_founded-Part R) \/ {x} by XBOOLE_0:def_3;
reconsider xwfp = (well_founded-Part R) \/ {x} as Subset of R ;
 {x} is well_founded Subset of R by Th6;
then A3: xwfp is well_founded by Th7;
assume  the InternalRel of R -Seg x c= well_founded-Part R ; ::_thesis: x in well_founded-Part R
then  xwfp is lower by Th5;
then  xwfp in  {  S where S is Subset of R : ( S is well_founded & S is lower )  }  by A3;
hence  x in well_founded-Part R by A1, A2, TARSKI:def_4; ::_thesis: verum
end;

scheme :: WELLFND1:sch 2
WFMin{ F1() ->  non empty RelStr , F2() ->  Element of F1(), P1[ set ] } :
 ex x being Element of F1() st
( P1[x] & ( for y being Element of F1() holds
( not x <> y or not P1[y] or not [y,x] in the InternalRel of F1() ) ) )
provided
A1: P1[F2()] and
A2: F1() is well_founded
proof
set c = the carrier of F1();
set r = the InternalRel of F1();
set Z =  {  x where x is Element of the carrier of F1() : P1[x]  }  ;
A3: F2() in  {  x where x is Element of the carrier of F1() : P1[x]  }  by A1;
  {  x where x is Element of the carrier of F1() : P1[x]  }  is Subset of the carrier of F1() from DOMAIN_1:sch_7();
then reconsider Z =  {  x where x is Element of the carrier of F1() : P1[x]  }  as non empty Subset of the carrier of F1() by A3;
 the InternalRel of F1() is_well_founded_in the carrier of F1() by A2, Def2;
then consider a being set  such that
A4: a in Z and
A5: the InternalRel of F1() -Seg a misses Z by WELLORD1:def_3;
reconsider a = a as Element of F1() by A4;
take  a ; ::_thesis: ( P1[a] & ( for y being Element of F1() holds
( not a <> y or not P1[y] or not [y,a] in the InternalRel of F1() ) ) )
 ex a9 being Element of the carrier of F1() st
( a9 = a & P1[a9] ) by A4;
hence  P1[a] ; ::_thesis: for y being Element of F1() holds
( not a <> y or not P1[y] or not [y,a] in the InternalRel of F1() )
given y being Element of F1() such that A6: ( a <> y & P1[y] & [y,a] in the InternalRel of F1() ) ; ::_thesis: contradiction
 ( y in Z & y in the InternalRel of F1() -Seg a ) by A6, WELLORD1:1;
hence  contradiction by A5, XBOOLE_0:3; ::_thesis: verum
end;

theorem Th10: :: WELLFND1:10
for R being non empty RelStr holds
( R is well_founded iff for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S )
proof
let R be non empty RelStr ; ::_thesis: ( R is well_founded iff for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S )
set c = the carrier of R;
set r = the InternalRel of R;
hereby  ::_thesis: ( ( for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S ) implies R is well_founded )
assume A1: R is well_founded ; ::_thesis: for S being set st ( for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S
let S be set ; ::_thesis: ( ( for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds
x in S ) implies the carrier of R c= S )
assume A2: for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds
x in S ; ::_thesis: the carrier of R c= S
defpred S1[ set ] means ( $1 in the carrier of R & not $1 in S );
assume  not the carrier of R c= S ; ::_thesis: contradiction
then consider x being set  such that
A3: x in the carrier of R and
A4: not x in S by TARSKI:def_3;
reconsider x = x as Element of R by A3;
A5: S1[x] by A4;
consider x0 being Element of R such that
A6: S1[x0] and
A7: for y being Element of R holds
( not x0 <> y or not S1[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch_2(A5, A1);
now__::_thesis:_the_InternalRel_of_R_-Seg_x0_c=_S
assume  not the InternalRel of R -Seg x0 c= S ; ::_thesis: contradiction
then consider z being set  such that
A8: z in the InternalRel of R -Seg x0 and
A9: not z in S by TARSKI:def_3;
A10: x0 <> z by A8, WELLORD1:1;
A11: [z,x0] in the InternalRel of R by A8, WELLORD1:1;
then reconsider z = z as Element of R by ZFMISC_1:87;
 z = z ;
hence  contradiction by A7, A9, A10, A11; ::_thesis: verum
end;
hence  contradiction by A2, A6; ::_thesis: verum
end;
assume A12: for S being set st ( for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S ; ::_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
A13: ( Y c= the carrier of R & Y <> {} ) and
A14: for a being set holds
( not a in Y or not the InternalRel of R -Seg a misses Y ) by WELLORD1:def_3;
now__::_thesis:_for_x_being_Element_of_the_carrier_of_R_st_the_InternalRel_of_R_-Seg_x_c=_the_carrier_of_R_\_Y_holds_
x_in_the_carrier_of_R_\_Y
let x be Element of the carrier of R; ::_thesis: ( the InternalRel of R -Seg x c= the carrier of R \ Y implies x in the carrier of R \ Y )
assume A15: the InternalRel of R -Seg x c= the carrier of R \ Y ; ::_thesis: x in the carrier of R \ Y
assume  not x in the carrier of R \ Y ; ::_thesis: contradiction
then  x in Y by XBOOLE_0:def_5;
then  the InternalRel of R -Seg x meets Y by A14;
then  ex z being set st
( z in the InternalRel of R -Seg x & z in Y ) by XBOOLE_0:3;
hence  contradiction by A15, XBOOLE_0:def_5; ::_thesis: verum
end;
then  the carrier of R c= the carrier of R \ Y by A12;
hence  contradiction by A13, XBOOLE_1:1, XBOOLE_1:38; ::_thesis: verum
end;

scheme :: WELLFND1:sch 3
WFInduction{ F1() ->  non empty RelStr , P1[ set ] } :
 for x being Element of F1() holds P1[x]
provided
A1: for x being Element of F1() st ( for y being Element of F1() st y <> x & [y,x] in the InternalRel of F1() holds
P1[y] ) holds
P1[x] and
A2: F1() is well_founded
proof
set c = the carrier of F1();
set r = the InternalRel of F1();
set Z =  {  x where x is Element of the carrier of F1() : P1[x]  }  ;
now__::_thesis:_for_x_being_Element_of_the_carrier_of_F1()_st_the_InternalRel_of_F1()_-Seg_x_c=__{__x_where_x_is_Element_of_the_carrier_of_F1()_:_P1[x]__}__holds_
x_in__{__x_where_x_is_Element_of_the_carrier_of_F1()_:_P1[x]__}_
let x be Element of the carrier of F1(); ::_thesis: ( the InternalRel of F1() -Seg x c=  {  x where x is Element of the carrier of F1() : P1[x]  }  implies x in  {  x where x is Element of the carrier of F1() : P1[x]  }  )
assume A3: the InternalRel of F1() -Seg x c=  {  x where x is Element of the carrier of F1() : P1[x]  }  ; ::_thesis: x in  {  x where x is Element of the carrier of F1() : P1[x]  }
reconsider x9 = x as Element of F1() ;
now__::_thesis:_for_y9_being_Element_of_F1()_st_y9_<>_x9_&_[y9,x9]_in_the_InternalRel_of_F1()_holds_
P1[y9]
let y9 be Element of F1(); ::_thesis: ( y9 <> x9 & [y9,x9] in the InternalRel of F1() implies P1[y9] )
assume  ( y9 <> x9 & [y9,x9] in the InternalRel of F1() ) ; ::_thesis: P1[y9]
then  y9 in the InternalRel of F1() -Seg x9 by WELLORD1:1;
then  y9 in  {  x where x is Element of the carrier of F1() : P1[x]  }  by A3;
then  ex y being Element of the carrier of F1() st
( y = y9 & P1[y] ) ;
hence  P1[y9] ; ::_thesis: verum
end;
then  P1[x9] by A1;
hence  x in  {  x where x is Element of the carrier of F1() : P1[x]  }  ; ::_thesis: verum
end;
then A4: the carrier of F1() c=  {  x where x is Element of the carrier of F1() : P1[x]  }  by A2, Th10;
let x be Element of F1(); ::_thesis: P1[x]
 x in the carrier of F1() ;
then  x in  {  x where x is Element of the carrier of F1() : P1[x]  }  by A4;
then  ex x9 being Element of the carrier of F1() st
( x = x9 & P1[x9] ) ;
hence  P1[x] ; ::_thesis: verum
end;

definition
let R be non empty RelStr ;
let V be non empty set ;
let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V;
let F be Function;
predF is_recursively_expressed_by H means :Def5: :: WELLFND1:def 5
 for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x)));
end;

:: deftheorem Def5 defines is_recursively_expressed_by WELLFND1:def_5_:_
 for R being non empty RelStr
for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F being Function holds
( F is_recursively_expressed_by H iff for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x))) );

theorem :: WELLFND1:11
for R being non empty RelStr holds
( R is well_founded iff for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H )
proof
let R be non empty RelStr ; ::_thesis: ( R is well_founded iff for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H )
set c = the carrier of R;
set r = the InternalRel of R;
defpred S1[] means  for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H;
reconsider ac = omega +` (card the carrier of R) as infinite Cardinal ;
set V = nextcard ac;
deffunc H1( Element of the carrier of R, Element of PFuncs ( the carrier of R,(nextcard ac))) ->  set = sup (rng $2);
A1: for x being Element of the carrier of R
for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H1(x,p) in nextcard ac
proof
let x be Element of the carrier of R; ::_thesis: for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H1(x,p) in nextcard ac
let p be Element of PFuncs ( the carrier of R,(nextcard ac)); ::_thesis: H1(x,p) in nextcard ac
 ( card (dom p) c= card the carrier of R & card (rng p) c= card (dom p) ) by CARD_1:11, CARD_1:12;
then A2: card (rng p) c= card the carrier of R by XBOOLE_1:1;
 card the carrier of R c= ac by CARD_2:94;
then  card (rng p) c= ac by A2, XBOOLE_1:1;
then A3: card (rng p) in nextcard ac by CARD_1:18, ORDINAL1:12;
 nextcard ac is regular by CARD_5:30;
hence  H1(x,p) in nextcard ac by A3, Th2; ::_thesis: verum
end;
consider H being Function of [: the carrier of R,(PFuncs ( the carrier of R,(nextcard ac))):],(nextcard ac) such that
A4: for x being Element of the carrier of R
for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H . (x,p) = H1(x,p) from FUNCT_7:sch_1(A1);
thus  ( R is well_founded implies S1[] ) ::_thesis: ( ( for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H ) implies R is well_founded )
proof
assume A5: R is well_founded ; ::_thesis: S1[]
let V be non empty set ; ::_thesis: for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H
let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V; ::_thesis: ex F being Function of the carrier of R,V st F is_recursively_expressed_by H
defpred S2[ PartFunc of the carrier of R,V] means ( dom $1 is lower & ( for x being set st x in dom $1 holds
$1 . x = H . [x,($1 | ( the InternalRel of R -Seg x))] ) );
consider fs being Subset of (PFuncs ( the carrier of R,V)) such that
A6: for f being PartFunc of the carrier of R,V holds
( f in fs iff S2[f] ) from WELLFND1:sch_1();
now__::_thesis:_for_f,_g_being_Function_st_f_in_fs_&_g_in_fs_holds_
f_tolerates_g
let f, g be Function; ::_thesis: ( f in fs & g in fs implies f tolerates g )
assume that
A7: f in fs and
A8: g in fs ; ::_thesis: f tolerates g
reconsider ff = f, gg = g as PartFunc of the carrier of R,V by A7, A8, PARTFUN1:46;
defpred S3[ set ] means ( $1 in dom ff & $1 in dom gg & ff . $1 <> gg . $1 );
assume  not f tolerates g ; ::_thesis: contradiction
then consider x being set  such that
A9: x in (dom ff) /\ (dom gg) and
A10: ff . x <> gg . x by PARTFUN1:def_4;
reconsider x = x as Element of R by A9;
A11: S3[x] by A9, A10, XBOOLE_0:def_4;
consider x0 being Element of R such that
A12: S3[x0] and
A13: for y being Element of R holds
( not x0 <> y or not S3[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch_2(A11, A5);
 ff | ( the InternalRel of R -Seg x0) = gg | ( the InternalRel of R -Seg x0)
proof
set fr = ff | ( the InternalRel of R -Seg x0);
set gr = gg | ( the InternalRel of R -Seg x0);
assume A14: not ff | ( the InternalRel of R -Seg x0) = gg | ( the InternalRel of R -Seg x0) ; ::_thesis: contradiction
A15: dom ff is lower by A6, A7;
then A16: dom (ff | ( the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 by A12, Th4, RELAT_1:62;
A17: dom gg is lower by A6, A8;
then  dom (ff | ( the InternalRel of R -Seg x0)) = dom (gg | ( the InternalRel of R -Seg x0)) by A12, A16, Th4, RELAT_1:62;
then consider x1 being set  such that
A18: x1 in dom (ff | ( the InternalRel of R -Seg x0)) and
A19: (ff | ( the InternalRel of R -Seg x0)) . x1 <> (gg | ( the InternalRel of R -Seg x0)) . x1 by A14, FUNCT_1:2;
A20: [x1,x0] in the InternalRel of R by A16, A18, WELLORD1:1;
reconsider x1 = x1 as Element of R by A18;
A21: ( (ff | ( the InternalRel of R -Seg x0)) . x1 = ff . x1 & (gg | ( the InternalRel of R -Seg x0)) . x1 = gg . x1 ) by A16, A18, FUNCT_1:49;
A22: x1 <> x0 by A16, A18, WELLORD1:1;
A23: x1 in dom gg by A12, A17, A20, Def1;
 x1 in dom ff by A12, A15, A20, Def1;
hence  contradiction by A13, A19, A20, A21, A22, A23; ::_thesis: verum
end;
then ff . x0 = H . [x0,(gg | ( the InternalRel of R -Seg x0))] by A6, A7, A12
.= gg . x0 by A6, A8, A12 ;
hence  contradiction by A12; ::_thesis: verum
end;
then reconsider ufs = union fs as Function by Th1;
A24: now__::_thesis:_for_x_being_set_st_x_in_dom_ufs_holds_
ufs_._x_=_H_._[x,(ufs_|_(_the_InternalRel_of_R_-Seg_x))]
let x be set ; ::_thesis: ( x in dom ufs implies ufs . x = H . [x,(ufs | ( the InternalRel of R -Seg x))] )
assume  x in dom ufs ; ::_thesis: ufs . x = H . [x,(ufs | ( the InternalRel of R -Seg x))]
then  [x,(ufs . x)] in ufs by FUNCT_1:1;
then consider fx being set  such that
A25: [x,(ufs . x)] in fx and
A26: fx in fs by TARSKI:def_4;
reconsider ff = fx as PartFunc of the carrier of R,V by A26, PARTFUN1:46;
A27: x in dom ff by A25, FUNCT_1:1;
A28: ( dom ff is lower & ff c= ufs ) by A6, A26, ZFMISC_1:74;
thus ufs . x = ff . x by A25, FUNCT_1:1
.= H . [x,(ff | ( the InternalRel of R -Seg x))] by A6, A26, A27
.= H . [x,(ufs | ( the InternalRel of R -Seg x))] by A27, A28, Th4, GRFUNC_1:27 ; ::_thesis: verum
end;
A29: dom ufs c= the carrier of R
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom ufs or y in the carrier of R )
assume  y in dom ufs ; ::_thesis: y in the carrier of R
then  [y,(ufs . y)] in ufs by FUNCT_1:1;
then consider fx being set  such that
A30: [y,(ufs . y)] in fx and
A31: fx in fs by TARSKI:def_4;
consider ff being Function such that
A32: ff = fx and
A33: dom ff c= the carrier of R and
 rng ff c= V by A31, PARTFUN1:def_3;
 y in dom ff by A30, A32, XTUPLE_0:def_12;
hence  y in the carrier of R by A33; ::_thesis: verum
end;
A34: rng ufs c= V
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ufs or y in V )
assume  y in rng ufs ; ::_thesis: y in V
then consider x being set  such that
A35: ( x in dom ufs & y = ufs . x ) by FUNCT_1:def_3;
 [x,y] in ufs by A35, FUNCT_1:1;
then consider fx being set  such that
A36: [x,y] in fx and
A37: fx in fs by TARSKI:def_4;
consider ff being Function such that
A38: ff = fx and
 dom ff c= the carrier of R and
A39: rng ff c= V by A37, PARTFUN1:def_3;
 y in rng ff by A36, A38, XTUPLE_0:def_13;
hence  y in V by A39; ::_thesis: verum
end;
A40: now__::_thesis:_for_x,_y_being_set_st_x_in_dom_ufs_&_[y,x]_in_the_InternalRel_of_R_holds_
y_in_dom_ufs
let x, y be set ; ::_thesis: ( x in dom ufs & [y,x] in the InternalRel of R implies y in dom ufs )
assume that
A41: x in dom ufs and
A42: [y,x] in the InternalRel of R ; ::_thesis: y in dom ufs
 [x,(ufs . x)] in ufs by A41, FUNCT_1:1;
then consider fx being set  such that
A43: [x,(ufs . x)] in fx and
A44: fx in fs by TARSKI:def_4;
reconsider ff = fx as PartFunc of the carrier of R,V by A44, PARTFUN1:46;
 ff c= ufs by A44, ZFMISC_1:74;
then A45: dom ff c= dom ufs by GRFUNC_1:2;
 ( dom ff is lower & x in dom ff ) by A6, A43, A44, FUNCT_1:1;
then  y in dom ff by A42, Def1;
hence  y in dom ufs by A45; ::_thesis: verum
end;
A46: dom ufs = the carrier of R
proof
defpred S3[ set ] means ( $1 in the carrier of R & not $1 in dom ufs );
assume  dom ufs <> the carrier of R ; ::_thesis: contradiction
then consider x being set  such that
A47: ( ( x in dom ufs & not x in the carrier of R ) or ( x in the carrier of R & not x in dom ufs ) ) by TARSKI:1;
reconsider x = x as Element of R by A29, A47;
A48: S3[x] by A47;
consider x0 being Element of R such that
A49: S3[x0] and
A50: for y being Element of R holds
( not x0 <> y or not S3[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch_2(A48, A5);
set nv = x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]);
set nf = ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]));
A51: dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) = {x0} by FUNCOP_1:13;
A52: rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= V
proof
 ufs in PFuncs ( the carrier of R,V) by A29, A34, PARTFUN1:def_3;
then  ufs is PartFunc of the carrier of R,V by PARTFUN1:46;
then  ufs | ( the InternalRel of R -Seg x0) is PartFunc of the carrier of R,V by PARTFUN1:11;
then A53: ufs | ( the InternalRel of R -Seg x0) in PFuncs ( the carrier of R,V) by PARTFUN1:45;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) or x in V )
assume A54: x in rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) ; ::_thesis: x in V
assume A55: not x in V ; ::_thesis: contradiction
then  ( rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= (rng ufs) \/ (rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) & not x in rng ufs ) by A34, FUNCT_4:17;
then A56: x in rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A54, XBOOLE_0:def_3;
 rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) = {(H . [x0,(ufs | ( the InternalRel of R -Seg x0))])} by FUNCOP_1:8;
then  x = H . (x0,(ufs | ( the InternalRel of R -Seg x0))) by A56, TARSKI:def_1;
hence  contradiction by A55, A53, BINOP_1:17; ::_thesis: verum
end;
A57: dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) = (dom ufs) \/ (dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) by FUNCT_4:def_1;
 dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= the carrier of R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) or x in the carrier of R )
assume that
A58: x in dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) and
A59: not x in the carrier of R ; ::_thesis: contradiction
 not x in dom ufs by A29, A59;
then  x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A57, A58, XBOOLE_0:def_3;
hence  contradiction by A51, A59; ::_thesis: verum
end;
then A60: ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) in PFuncs ( the carrier of R,V) by A52, PARTFUN1:def_3;
 x0 in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A51, TARSKI:def_1;
then  x0 in dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) by A57, XBOOLE_0:def_3;
then A61: [x0,((ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) . x0)] in ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by FUNCT_1:1;
reconsider nf = ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) as PartFunc of the carrier of R,V by A60, PARTFUN1:46;
A62: now__::_thesis:_for_x_being_set_st_x_in_dom_nf_holds_
nf_._x_=_H_._[x,(nf_|_(_the_InternalRel_of_R_-Seg_x))]
let x be set ; ::_thesis: ( x in dom nf implies nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))] )
assume A63: x in dom nf ; ::_thesis: nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))]
percases ( x in dom ufs or x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) ) by A57, A63, XBOOLE_0:def_3;
supposeA64: x in dom ufs ; ::_thesis: nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))]
A65: {x0} misses the InternalRel of R -Seg x
proof
assume  {x0} meets the InternalRel of R -Seg x ; ::_thesis: contradiction
then consider y being set  such that
A66: y in {x0} and
A67: y in the InternalRel of R -Seg x by XBOOLE_0:3;
 y = x0 by A66, TARSKI:def_1;
then  [x0,x] in the InternalRel of R by A67, WELLORD1:1;
hence  contradiction by A40, A49, A64; ::_thesis: verum
end;
 not x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A49, A64, TARSKI:def_1;
hence nf . x = ufs . x by FUNCT_4:11
.= H . [x,(ufs | ( the InternalRel of R -Seg x))] by A24, A64
.= H . [x,(nf | ( the InternalRel of R -Seg x))] by A51, A65, FUNCT_4:72 ;
::_thesis: verum
end;
supposeA68: x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) ; ::_thesis: nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))]
A69: {x0} misses the InternalRel of R -Seg x0
proof
assume  {x0} meets the InternalRel of R -Seg x0 ; ::_thesis: contradiction
then consider x being set  such that
A70: x in {x0} and
A71: x in the InternalRel of R -Seg x0 by XBOOLE_0:3;
 x = x0 by A70, TARSKI:def_1;
hence  contradiction by A71, WELLORD1:1; ::_thesis: verum
end;
A72: x = x0 by A68, TARSKI:def_1;
hence nf . x = (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) . x0 by A68, FUNCT_4:13
.= H . [x0,(ufs | ( the InternalRel of R -Seg x0))] by FUNCOP_1:72
.= H . [x,(nf | ( the InternalRel of R -Seg x))] by A51, A72, A69, FUNCT_4:72 ;
::_thesis: verum
end;
end;
end;
 dom nf is lower
proof
let x, y be set ; :: according to WELLFND1:def_1 ::_thesis: ( x in dom nf & [y,x] in the InternalRel of R implies y in dom nf )
assume that
A73: x in dom nf and
A74: [y,x] in the InternalRel of R ; ::_thesis: y in dom nf
assume A75: not y in dom nf ; ::_thesis: contradiction
then A76: not y in dom ufs by A57, XBOOLE_0:def_3;
then  not x in dom ufs by A40, A74;
then  x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A57, A73, XBOOLE_0:def_3;
then A77: x = x0 by TARSKI:def_1;
reconsider y = y as Element of R by A74, ZFMISC_1:87;
 not y in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A57, A75, XBOOLE_0:def_3;
then  y <> x0 by A51, TARSKI:def_1;
hence  contradiction by A50, A74, A76, A77; ::_thesis: verum
end;
then  nf in fs by A6, A62;
then  [x0,(nf . x0)] in ufs by A61, TARSKI:def_4;
hence  contradiction by A49, FUNCT_1:1; ::_thesis: verum
end;
then reconsider ufs = ufs as Function of the carrier of R,V by A34, FUNCT_2:def_1, RELSET_1:4;
take  ufs ; ::_thesis: ufs is_recursively_expressed_by H
let x be Element of the carrier of R; :: according to WELLFND1:def_5 ::_thesis: ufs . x = H . (x,(ufs | ( the InternalRel of R -Seg x)))
thus  ufs . x = H . (x,(ufs | ( the InternalRel of R -Seg x))) by A24, A46; ::_thesis: verum
end;
assume  S1[] ; ::_thesis: R is well_founded
then consider rk being Function of the carrier of R,(nextcard ac) such that
A78: rk is_recursively_expressed_by H ;
let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_2 ::_thesis: ( not Y c= the carrier of R or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )
assume that
A79: Y c= the carrier of R and
A80: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )
set m = inf (rk .: Y);
consider b being set  such that
A81: b in Y by A80, XBOOLE_0:def_1;
A82: dom rk = the carrier of R by FUNCT_2:def_1;
then  rk . b in rk .: Y by A79, A81, FUNCT_1:def_6;
then  inf (rk .: Y) in rk .: Y by ORDINAL2:17;
then consider a being set  such that
A83: a in dom rk and
A84: a in Y and
A85: rk . a = inf (rk .: Y) by FUNCT_1:def_6;
take  a ; ::_thesis: ( a in Y & the InternalRel of R -Seg a misses Y )
thus  a in Y by A84; ::_thesis: the InternalRel of R -Seg a misses Y
assume  ( the InternalRel of R -Seg a) /\ Y <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider e being set  such that
A86: e in ( the InternalRel of R -Seg a) /\ Y by XBOOLE_0:def_1;
A87: e in the InternalRel of R -Seg a by A86, XBOOLE_0:def_4;
reconsider a = a as Element of the carrier of R by A83;
reconsider rkra = rk | ( the InternalRel of R -Seg a) as Element of PFuncs ( the carrier of R,(nextcard ac)) by PARTFUN1:45;
A88: rk . a = H . (a,rkra) by A78, Def5
.= sup (rng rkra) by A4 ;
A89: e in Y by A86, XBOOLE_0:def_4;
then reconsider rke = rk . e as Ordinal by A79, FUNCT_2:5, ORDINAL1:13;
 rke in rk .: Y by A82, A79, A89, FUNCT_1:def_6;
then A90: inf (rk .: Y) c= rk . e by ORDINAL2:14;
 rke in rng rkra by A82, A79, A87, A89, FUNCT_1:50;
hence  contradiction by A85, A90, A88, ORDINAL1:5, ORDINAL2:19; ::_thesis: verum
end;

theorem :: WELLFND1:12
for R being non empty RelStr
for V being non trivial set st ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2 ) holds
R is well_founded
proof
let R be non empty RelStr ; ::_thesis: for V being non trivial set st ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2 ) holds
R is well_founded
let V be non trivial set ; ::_thesis: ( ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2 ) implies R is well_founded )
set c = the carrier of R;
set r = the InternalRel of R;
set PF = PFuncs ( the carrier of R,V);
set wfp = well_founded-Part R;
consider a0, a1 being set  such that
A1: a0 in V and
A2: a1 in V and
A3: a0 <> a1 by ZFMISC_1:def_10;
set F3 = the carrier of R --> a1;
set F4 = (well_founded-Part R) --> a0;
set F2 = ( the carrier of R --> a1) +* ((well_founded-Part R) --> a0);
A4: dom ( the carrier of R --> a1) = the carrier of R by FUNCOP_1:13;
defpred S1[ set , Function, set ] means ( ex x being set st
( x in dom $2 & $2 . x = a1 ) iff $3 = a1 );
set a01 = {a0,a1};
A5: now__::_thesis:_for_x_being_Element_of_the_carrier_of_R
for_y_being_Element_of_PFuncs_(_the_carrier_of_R,V)_ex_u_being_Element_of_{a0,a1}_st_S1[x,y,u]
reconsider u = a1, v = a0 as Element of {a0,a1} by TARSKI:def_2;
let x be Element of the carrier of R; ::_thesis: for y being Element of PFuncs ( the carrier of R,V) ex u being Element of {a0,a1} st S1[u,b3,b4]
let y be Element of PFuncs ( the carrier of R,V); ::_thesis: ex u being Element of {a0,a1} st S1[u,b2,b3]
percases ( ex x being set st
( x in dom y & y . x = a1 ) or for x being set holds
( not x in dom y or not y . x = a1 ) ) ;
supposeA6: ex x being set st
( x in dom y & y . x = a1 ) ; ::_thesis: ex u being Element of {a0,a1} st S1[u,b2,b3]
take u = u; ::_thesis: S1[x,y,u]
thus  S1[x,y,u] by A6; ::_thesis: verum
end;
supposeA7: for x being set holds
( not x in dom y or not y . x = a1 ) ; ::_thesis: ex v being Element of {a0,a1} st S1[v,b2,b3]
take v = v; ::_thesis: S1[x,y,v]
thus  S1[x,y,v] by A3, A7; ::_thesis: verum
end;
end;
end;
consider H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],{a0,a1} such that
A8: for x being Element of the carrier of R
for y being Element of PFuncs ( the carrier of R,V) holds S1[x,y,H . (x,y)] from BINOP_1:sch_3(A5);
A9: {a0,a1} c= V by A1, A2, ZFMISC_1:32;
then A10: rng H c= V by XBOOLE_1:1;
 (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0} \/ {a1} by XBOOLE_1:13;
then A11: (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0,a1} by ENUMSET1:1;
 rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) by FUNCT_4:17;
then  rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= {a0,a1} by A11, XBOOLE_1:1;
then A12: rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= V by A9, XBOOLE_1:1;
A13: rng H c= {a0,a1} ;
A14: dom H = [: the carrier of R,(PFuncs ( the carrier of R,V)):] by FUNCT_2:def_1;
then reconsider H = H as Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V by A10, FUNCT_2:def_1, RELSET_1:4;
A15: dom ((well_founded-Part R) --> a0) = well_founded-Part R by FUNCOP_1:13;
A16: dom (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) = (dom ( the carrier of R --> a1)) \/ (dom ((well_founded-Part R) --> a0)) by FUNCT_4:def_1
.= the carrier of R by A4, A15, XBOOLE_1:12 ;
then reconsider F2 = ( the carrier of R --> a1) +* ((well_founded-Part R) --> a0) as Function of the carrier of R,V by A12, FUNCT_2:def_1, RELSET_1:4;
A17: F2 is_recursively_expressed_by H
proof
let x be Element of the carrier of R; :: according to WELLFND1:def_5 ::_thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x)))
reconsider F2r = F2 | ( the InternalRel of R -Seg x) as Element of PFuncs ( the carrier of R,V) by PARTFUN1:45;
percases ( x in well_founded-Part R or not x in well_founded-Part R ) ;
supposeA18: x in well_founded-Part R ; ::_thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x)))
now__::_thesis:_for_z_being_set_st_z_in_dom_F2r_holds_
F2r_._z_<>_a1
let z be set ; ::_thesis: ( z in dom F2r implies F2r . z <> a1 )
A19: the InternalRel of R -Seg x c= well_founded-Part R by A18, Th4;
assume  z in dom F2r ; ::_thesis: F2r . z <> a1
then A20: z in the InternalRel of R -Seg x by RELAT_1:57;
then F2r . z = F2 . z by FUNCT_1:49
.= ((well_founded-Part R) --> a0) . z by A15, A20, A19, FUNCT_4:13
.= a0 by A20, A19, FUNCOP_1:7 ;
hence  F2r . z <> a1 by A3; ::_thesis: verum
end;
then A21: H . (x,F2r) <> a1 by A8;
A22: H . [x,F2r] in rng H by A14, FUNCT_1:def_3;
 ((well_founded-Part R) --> a0) . x = a0 by A18, FUNCOP_1:7;
hence F2 . x = a0 by A15, A18, FUNCT_4:13
.= H . (x,(F2 | ( the InternalRel of R -Seg x))) by A13, A21, A22, TARSKI:def_2 ;
::_thesis: verum
end;
supposeA23: not x in well_founded-Part R ; ::_thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x)))
then  not the InternalRel of R -Seg x c= well_founded-Part R by Th9;
then consider z being set  such that
A24: z in the InternalRel of R -Seg x and
A25: not z in well_founded-Part R by TARSKI:def_3;
A26: the InternalRel of R -Seg x c= the carrier of R by Th3;
then A27: z in dom F2r by A16, A24, RELAT_1:57;
A28: F2r . z = F2 . z by A24, FUNCT_1:49
.= ( the carrier of R --> a1) . z by A15, A25, FUNCT_4:11
.= a1 by A24, A26, FUNCOP_1:7 ;
thus F2 . x = ( the carrier of R --> a1) . x by A15, A23, FUNCT_4:11
.= a1 by FUNCOP_1:7
.= H . (x,(F2 | ( the InternalRel of R -Seg x))) by A8, A27, A28 ; ::_thesis: verum
end;
end;
end;
reconsider F1 = the carrier of R --> a0 as Function of the carrier of R,V by A1, FUNCOP_1:45;
assume A29: for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2 ; ::_thesis: R is well_founded
assume  not R is well_founded ; ::_thesis: contradiction
then  well_founded-Part R <> the carrier of R by Th8;
then consider x being set  such that
A30: ( ( x in well_founded-Part R & not x in the carrier of R ) or ( x in the carrier of R & not x in well_founded-Part R ) ) by TARSKI:1;
A31: F1 is_recursively_expressed_by H
proof
let x be Element of the carrier of R; :: according to WELLFND1:def_5 ::_thesis: F1 . x = H . (x,(F1 | ( the InternalRel of R -Seg x)))
reconsider F1r = F1 | ( the InternalRel of R -Seg x) as Element of PFuncs ( the carrier of R,V) by PARTFUN1:45;
A32: H . [x,F1r] in rng H by A14, FUNCT_1:def_3;
now__::_thesis:_for_z_being_set_st_z_in_dom_F1r_holds_
F1r_._z_<>_a1
let z be set ; ::_thesis: ( z in dom F1r implies F1r . z <> a1 )
assume A33: z in dom F1r ; ::_thesis: F1r . z <> a1
then  z in the InternalRel of R -Seg x by RELAT_1:57;
then F1r . z = F1 . z by FUNCT_1:49
.= a0 by A33, FUNCOP_1:7 ;
hence  F1r . z <> a1 by A3; ::_thesis: verum
end;
then A34: H . (x,F1r) <> a1 by A8;
thus F1 . x = a0 by FUNCOP_1:7
.= H . (x,(F1 | ( the InternalRel of R -Seg x))) by A13, A34, A32, TARSKI:def_2 ; ::_thesis: verum
end;
A35: F1 . x = a0 by A30, FUNCOP_1:7;
F2 . x = ( the carrier of R --> a1) . x by A15, A30, FUNCT_4:11
.= a1 by A30, FUNCOP_1:7 ;
hence  contradiction by A3, A31, A17, A29, A35; ::_thesis: verum
end;

theorem :: WELLFND1:13
for R being non empty well_founded RelStr
for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2
proof
let R be non empty well_founded RelStr ; ::_thesis: for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2
let V be non empty set ; ::_thesis: for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2
set c = the carrier of R;
set r = the InternalRel of R;
let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V; ::_thesis: for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2
let F1, F2 be Function of the carrier of R,V; ::_thesis: ( F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H implies F1 = F2 )
assume that
A1: F1 is_recursively_expressed_by H and
A2: F2 is_recursively_expressed_by H ; ::_thesis: F1 = F2
defpred S1[ set ] means F1 . $1 <> F2 . $1;
A3: dom F2 = the carrier of R by FUNCT_2:def_1;
assume  F1 <> F2 ; ::_thesis: contradiction
then consider x being Element of the carrier of R such that
A4: F1 . x <> F2 . x by FUNCT_2:63;
reconsider x = x as Element of R ;
A5: R is well_founded ;
A6: S1[x] by A4;
consider x0 being Element of R such that
A7: S1[x0] and
A8: for y being Element of R holds
( not x0 <> y or not S1[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch_2(A6, A5);
A9: dom F1 = the carrier of R by FUNCT_2:def_1;
 F1 | ( the InternalRel of R -Seg x0) = F2 | ( the InternalRel of R -Seg x0)
proof
set fr = F1 | ( the InternalRel of R -Seg x0);
set gr = F2 | ( the InternalRel of R -Seg x0);
assume A10: not F1 | ( the InternalRel of R -Seg x0) = F2 | ( the InternalRel of R -Seg x0) ; ::_thesis: contradiction
A11: dom (F1 | ( the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 by A9, Th3, RELAT_1:62;
 dom (F2 | ( the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 by A3, Th3, RELAT_1:62;
then consider x1 being set  such that
A12: x1 in dom (F1 | ( the InternalRel of R -Seg x0)) and
A13: (F1 | ( the InternalRel of R -Seg x0)) . x1 <> (F2 | ( the InternalRel of R -Seg x0)) . x1 by A11, A10, FUNCT_1:2;
A14: [x1,x0] in the InternalRel of R by A11, A12, WELLORD1:1;
reconsider x1 = x1 as Element of R by A12;
A15: x1 <> x0 by A11, A12, WELLORD1:1;
 ( (F1 | ( the InternalRel of R -Seg x0)) . x1 = F1 . x1 & (F2 | ( the InternalRel of R -Seg x0)) . x1 = F2 . x1 ) by A11, A12, FUNCT_1:49;
hence  contradiction by A8, A13, A14, A15; ::_thesis: verum
end;
then F1 . x0 = H . (x0,(F2 | ( the InternalRel of R -Seg x0))) by A1, Def5
.= F2 . x0 by A2, Def5 ;
hence  contradiction by A7; ::_thesis: verum
end;

definition
let R be RelStr ;
let f be sequence of R;
attrf is descending  means :Def6: :: WELLFND1:def 6
 for n being Nat holds
( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R );
end;

:: deftheorem Def6 defines descending WELLFND1:def_6_:_
 for R being RelStr
for f being sequence of R holds
( f is descending iff for n being Nat holds
( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) );

theorem :: WELLFND1:14
for R being non empty RelStr holds
( R is well_founded iff for f being sequence of R holds not f is descending )
proof
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 by FUNCT_2:def_1;
then  rng f <> {} by RELAT_1:42;
then consider a being set  such that
A4: a in rng f and
A5: the InternalRel of R -Seg a misses rng f by A1, WELLORD1:def_3;
consider n being set  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, Def6;
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 by Def2;
then consider Y being set  such that
A10: Y c= the carrier of R and
A11: Y <> {} and
A12: for a being set holds
( not a in Y or the InternalRel of R -Seg a meets Y ) by WELLORD1:def_3;
deffunc H1( 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
A13: dom f = NAT and
A14: f . 0 = choose 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 <> {} by XBOOLE_0:def_7;
 f . (n + 1) = choose (( the InternalRel of R -Seg (f . n)) /\ Y) by A15;
hence  S1[n + 1] by A17, XBOOLE_0:def_4; ::_thesis: verum
end;
A18: S1[ 0 ] by A11, A14;
A19: for n being Nat holds S1[n] from NAT_1:sch_2(A18, A16);
 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
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 <> {} by XBOOLE_0:def_7;
 f . (n + 1) = choose (( 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 by Def6;
hence  contradiction by A9; ::_thesis: verum
end;