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 Th7;
then A3: xwfp is well_founded by Th8;
assume the InternalRel of R -Seg x c= well_founded-Part R ; :: thesis: x in well_founded-Part R
then xwfp is lower by Th6;
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