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

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