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 b₁ being set st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y ) )
assume that
A4: Y c= the carrier of R and
A5: Y <> {} ; :: thesis: ex b₁ being set st
( b₁ in Y & the InternalRel of R -Seg b₁ 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, Th5, 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 b₁ being set st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y ) by A14; :: thesis: verum