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;

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_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} misses Y ) )

assume that

A4: Y c= the carrier of R and

A5: Y <> {} ; :: thesis: ex b_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} misses Y )

consider y being object 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;

( Y /\ S c= S & Y /\ S <> {} ) by A6, A7, A9, XBOOLE_0:def 4;

then consider a being object such that

A12: a in Y /\ S and

A13: the InternalRel of R -Seg a misses Y /\ S by A11;

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;

then the InternalRel of R -Seg a misses Y by A15;

hence ex b_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} misses Y )
by A14; :: thesis: verum

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 )

assume A3:
well_founded-Part R = the carrier of R
; :: thesis: R is well_founded A2:
cs is lower
;

assume R is well_founded ; :: thesis: well_founded-Part R = the carrier of R

then the InternalRel of R is_well_founded_in cs ;

then cs is well_founded ;

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 ; :: 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 ;

then cs is well_founded ;

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 ; :: thesis: verum

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

( b

assume that

A4: Y c= the carrier of R and

A5: Y <> {} ; :: thesis: ex b

( b

consider y being object 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;

( Y /\ S c= S & Y /\ S <> {} ) by A6, A7, A9, XBOOLE_0:def 4;

then consider a being object such that

A12: a in Y /\ S and

A13: the InternalRel of R -Seg a misses Y /\ S by A11;

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;

then the InternalRel of R -Seg a misses Y by A15;

hence ex b

( b