A1: field R = field (R ~) by RELAT_1:21;

hereby :: thesis:

assume R is co-well_founded ; :: thesis:
then A2: R ~ is well_founded ;
let Y be set ; :: thesis:
assume ( Y c= field R & Y <> {} ) ; :: thesis:
then consider a being object such that
A3: a in Y and
A4: (R ~) -Seg a misses Y by A1, A2;
take a = a; :: thesis:
thus a in Y by A3; :: thesis:
let b be object ; :: thesis:
assume b in Y ; :: thesis:
then not b in (R ~) -Seg a by A4, XBOOLE_0:3;
then ( a = b or not [b,a] in R ~ ) by WELLORD1:1;
hence ( a <> b implies not [a,b] in R ) by RELAT_1:def 7; :: thesis:

end;

hereby :: thesis:

assume A5: for Y being set st Y c= field R & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) ) ; :: thesis:
R ~ is well_founded

proof

let Y be set ; :: according to WELLORD1:def 2 :: thesis:
assume ( Y c= field (R ~) & Y <> {} ) ; :: thesis:
then consider a being object such that
A6: a in Y and
A7: for b being object st b in Y & a <> b holds
not [a,b] in R by A1, A5;
take a ; :: thesis:
thus a in Y by A6; :: thesis:

now :: thesis:

assume not ((R ~) -Seg a) /\ Y is empty ; :: thesis:
then reconsider A = ((R ~) -Seg a) /\ Y as non empty set ;
set x = the Element of A;
A8: the Element of A in (R ~) -Seg a by XBOOLE_0:def 4;
then ( the Element of A in Y & the Element of A <> a ) by WELLORD1:1, XBOOLE_0:def 4;
then A9: not [a, the Element of A] in R by A7;
[ the Element of A,a] in R ~ by A8, WELLORD1:1;
hence contradiction by A9, RELAT_1:def 7; :: thesis:

end;

hence (R ~) -Seg a misses Y by XBOOLE_0:def 7; :: thesis:

end;

hence R is co-well_founded ; :: thesis:

end;