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

hereby :: thesis: ( ( for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set 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 set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
then A2: R ~ is well_founded by Def13;
let Y be set ; :: thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) )
assume ( Y c= field R & Y <> {} ) ; :: thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
then consider a being set such that
A3: a in Y and
A4: (R ~ ) -Seg a misses Y by A1, A2, WELLORD1:def 2;
take a = a; :: thesis: ( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
thus a in Y by A3; :: thesis: for b being set st b in Y & a <> b holds
not [a,b] in R
let b be set ; :: 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:def 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 set st
( a in Y & ( for b being set 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 set st
( b₁ in Y & (R ~ ) -Seg b₁ misses Y ) )
assume ( Y c= field (R ~ ) & Y <> {} ) ; :: thesis: ex b₁ being set st
( b₁ in Y & (R ~ ) -Seg b₁ misses Y )
then consider a being set such that
A6: a in Y and
A7: for b being set 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

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

end;