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;

_{1} being object st

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

assume that

A8: Y c= well_founded-Part R and

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

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;

( Y /\ S c= S & Y /\ S <> {} ) by A10, A11, A13, XBOOLE_0:def 4;

then consider a being object such that

A16: a in Y /\ S and

A17: the InternalRel of R -Seg a misses Y /\ S by A15;

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;

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

hence ex b_{1} being object st

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

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 Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 3 :: thesis: ( not Y c= well_founded-Part R or Y = {} or ex blet x, y be object ; :: 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;

hence y in well_founded-Part R by A1, A5, A6, TARSKI:def 4; :: thesis: verum

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

hence y in well_founded-Part R by A1, A5, A6, TARSKI:def 4; :: thesis: verum

( b

assume that

A8: Y c= well_founded-Part R and

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

( b

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

( Y /\ S c= S & Y /\ S <> {} ) by A10, A11, A13, XBOOLE_0:def 4;

then consider a being object such that

A16: a in Y /\ S and

A17: the InternalRel of R -Seg a misses Y /\ S by A15;

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;

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

hence ex b

( b