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 WELLFND1:def 1 well_founded-Part R is well_founded
let x,
y be
object ;
( 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
;
y in well_founded-Part Rconsider 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;
verum
end;
let Y be set ; WELLORD1:def 3,WELLFND1:def 3 ( 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 <> {}
; 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 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 b1 being object st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )
by A18; verum