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;

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 ) ;

hence contradiction by A13, XBOOLE_1:1, XBOOLE_1:38; :: thesis: verum

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 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 ) 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_{1}[ 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_{1}[x]
by A4;

consider x0 being Element of R such that

A6: S_{1}[x0]
and

A7: for y being Element of R holds

( not x0 <> y or not S_{1}[y] or not [y,x0] in the InternalRel of R )
from WELLFND1:sch 2(A5, A1);

end;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

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

consider x0 being Element of R such that

A6: S

A7: for y being Element of R holds

( not x0 <> y or not S

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

hence
contradiction
by A2, A6; :: thesis: verumassume
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;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

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

then
the carrier of R c= the carrier of R \ Y
by A12;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;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

hence contradiction by A13, XBOOLE_1:1, XBOOLE_1:38; :: thesis: verum