let R be non empty RelStr ; :: thesis: ( R is well_founded iff for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S )
set c = the carrier of R;
set r = the InternalRel of R;

hereby :: thesis: ( ( for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S ) implies R is well_founded )

assume A1: R is well_founded ; :: thesis: for S being set st ( for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S
let S be set ; :: thesis: ( ( for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds
x in S ) implies the carrier of R c= S )
assume A2: for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds
x in S ; :: thesis: the carrier of R c= S
assume not the carrier of R c= S ; :: thesis: contradiction
then consider x being set such that
A3: ( x in the carrier of R & not x in S ) by TARSKI:def 3;
reconsider x = x as Element of R by A3;
defpred S₁[ set ] means ( $1 in the carrier of R & not $1 in S );
A4: S₁[x] by A3;
consider x0 being Element of R such that
A5: S₁[x0] and
A6: for y being Element of R holds
( not x0 <> y or not S₁[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch 2(A4, A1);

now

assume not the InternalRel of R -Seg x0 c= S ; :: thesis: contradiction
then consider z being set such that
A7: ( z in the InternalRel of R -Seg x0 & not z in S ) by TARSKI:def 3;
A8: ( x0 <> z & [z,x0] in the InternalRel of R ) by A7, WELLORD1:def 1;
then reconsider z = z as Element of R by ZFMISC_1:106;
z = z ;
hence contradiction by A6, A7, A8; :: thesis: verum

end;

hence contradiction by A2, A5; :: thesis: verum

end;

assume A9: for S being set st ( for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S ; :: thesis: R is well_founded
assume not R is well_founded ; :: thesis: contradiction
then not the InternalRel of R is_well_founded_in the carrier of R by Def2;
then consider Y being set such that
A10: ( Y c= the carrier of R & Y <> {} ) and
A11: for a being set holds
( not a in Y or not the InternalRel of R -Seg a misses Y ) by WELLORD1:def 3;

now

let x be Element of the carrier of R; :: thesis: ( the InternalRel of R -Seg x c= the carrier of R \ Y implies x in the carrier of R \ Y )
assume A12: the InternalRel of R -Seg x c= the carrier of R \ Y ; :: thesis: x in the carrier of R \ Y
assume not x in the carrier of R \ Y ; :: thesis: contradiction
then x in Y by XBOOLE_0:def 5;
then the InternalRel of R -Seg x meets Y by A11;
then consider z being set such that
A13: ( z in the InternalRel of R -Seg x & z in Y ) by XBOOLE_0:3;
thus contradiction by A12, A13, XBOOLE_0:def 5; :: thesis: verum

end;

then the carrier of R c= the carrier of R \ Y by A9;
hence contradiction by A10, XBOOLE_1:1, XBOOLE_1:38; :: thesis: verum