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 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:
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 ;
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 ; :: thesis: verum
end;
let Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 3 :: thesis: ( not Y c= well_founded-Part R or Y = {} or ex b1 being object st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )

assume that
A8: Y c= well_founded-Part R and
A9: Y <> {} ; :: thesis: ex b1 being object st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )

consider y being object such that
A10: y in Y by ;
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 ;
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 ;
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 ;
a in S by ;
then A19: ( the InternalRel of R -Seg a) /\ Y = (( the InternalRel of R -Seg a) /\ S) /\ Y by
.= ( 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 b1 being object st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) by A18; :: thesis: verum