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
defpred S₁[ set ] means ( $1 in the carrier of R & not $1 in S );
assume not the carrier of R c= S ; :: thesis: contradiction
then consider x being object such that
A3: x in the carrier of R and
A4: not x in S ;
reconsider x = x as Element of R by A3;
A5: S₁[x] by A4;
consider x0 being Element of R such that
A6: S₁[x0] and
A7: 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(A5, A1);

now :: thesis: the InternalRel of R -Seg x0 c= S

assume not the InternalRel of R -Seg x0 c= S ; :: thesis: contradiction
then consider z being object such that
A8: z in the InternalRel of R -Seg x0 and
A9: not z in S ;
A10: x0 <> z by A8, WELLORD1:1;
A11: [z,x0] in the InternalRel of R by A8, WELLORD1:1;
then reconsider z = z as Element of R by ZFMISC_1:87;
z = z ;
hence contradiction by A7, A9, A10, A11; :: thesis: verum

end;

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

end;

assume A12: 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 ;
then consider Y being set such that
A13: ( Y c= the carrier of R & Y <> {} ) and
A14: for a being object holds
( not a in Y or not the InternalRel of R -Seg a misses Y ) ;

now :: thesis: for x being Element of the carrier of R st the InternalRel of R -Seg x c= the carrier of R \ Y holds
x in the carrier of R \ Y

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 A15: 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 A14;
then ex z being object st
( z in the InternalRel of R -Seg x & z in Y ) by XBOOLE_0:3;
hence contradiction by A15, XBOOLE_0:def 5; :: thesis: verum

end;

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