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;

hereby :: according to WELLFND1:def 1 :: thesis:

let x, y be set ; :: thesis:
assume A2: ( x in well_founded-Part R & [y,x] in the InternalRel of R ) ; :: thesis:
then consider Y being set such that
A3: ( x in Y & Y in { S where S is Subset of R : ( S is well_founded & S is lower ) } ) by A1, TARSKI:def 4;
consider S being Subset of R such that
A4: ( Y = S & S is well_founded & S is lower ) by A3;
y in S by A2, A3, A4, Def1;
hence y in well_founded-Part R by A1, A3, A4, TARSKI:def 4; :: thesis:

end;

let Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 3 :: thesis:
assume A5: ( Y c= well_founded-Part R & Y <> {} ) ; :: thesis:
then consider y being set such that
A6: y in Y by XBOOLE_0:def 1;
consider YY being set such that
A7: ( y in YY & YY in { S where S is Subset of R : ( S is well_founded & S is lower ) } ) by A1, A5, A6, TARSKI:def 4;
consider S being Subset of R such that
A8: ( YY = S & S is well_founded & S is lower ) by A7;
A9: the InternalRel of R is_well_founded_in S by A8, Def3;
set YS = Y /\ S;
( Y /\ S c= S & Y /\ S <> {} ) by A6, A7, A8, XBOOLE_0:def 4, XBOOLE_1:17;
then consider a being set such that
A10: ( a in Y /\ S & the InternalRel of R -Seg a misses Y /\ S ) by A9, WELLORD1:def 3;
A11: ( a in Y & a in S ) by A10, XBOOLE_0:def 4;
then A12: (the InternalRel of R -Seg a) /\ Y = ((the InternalRel of R -Seg a) /\ S) /\ Y by A8, 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 A10, XBOOLE_0:def 7;
then the InternalRel of R -Seg a misses Y by A12, XBOOLE_0:def 7;
hence ex b₁ being set st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y ) by A11; :: thesis: