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

hereby :: thesis: ( ( 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 ) ) ) implies R is co-well_founded )

assume R is co-well_founded ; :: thesis: 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 ) )
then A2: R ~ is well_founded ;
let Y be set ; :: thesis: ( Y c= field R & Y <> {} implies ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) ) )
assume ( Y c= field R & Y <> {} ) ; :: thesis: ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) )
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: ( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) )
thus a in Y by A3; :: thesis: for b being object st b in Y & a <> b holds
not [a,b] in R
let b be object ; :: thesis: ( b in Y & a <> b implies not [a,b] in R )
assume b in Y ; :: thesis: ( a <> b implies not [a,b] in R )
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: verum

end;

hereby :: thesis: verum

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 co-well_founded
R ~ is well_founded

proof

let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( not Y c= field (R ~) or Y = {} or ex b₁ being object st
( b₁ in Y & (R ~) -Seg b₁ misses Y ) )
assume ( Y c= field (R ~) & Y <> {} ) ; :: thesis: ex b₁ being object st
( b₁ in Y & (R ~) -Seg b₁ misses Y )
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: ( a in Y & (R ~) -Seg a misses Y )
thus a in Y by A6; :: thesis: (R ~) -Seg a misses Y

now :: thesis: ((R ~) -Seg a) /\ Y is empty

assume not ((R ~) -Seg a) /\ Y is empty ; :: thesis: contradiction
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: verum

end;

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

end;

hence R is co-well_founded ; :: thesis: verum

end;