let R be Relation; :: thesis: for A being set st R well_orders A holds
( R |_2 A well_orders A & A = field (R |_2 A) )
let A be set ; :: thesis: ( R well_orders A implies ( R |_2 A well_orders A & A = field (R |_2 A) ) )
assume A1: R well_orders A ; :: thesis: ( R |_2 A well_orders A & A = field (R |_2 A) )
then A2: R is_reflexive_in A ;
A3: R |_2 A is_reflexive_in A

proof

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in A or [x,x] in R |_2 A )
assume x in A ; :: thesis: [x,x] in R |_2 A
then ( [x,x] in R & [x,x] in [:A,A:] ) by A2, ZFMISC_1:87;
hence [x,x] in R |_2 A by XBOOLE_0:def 4; :: thesis: verum

end;

A4: R |_2 A is_connected_in A

proof

let x, y be object ; :: according to RELAT_2:def 6 :: thesis: ( not x in A or not y in A or x = y or [x,y] in R |_2 A or [y,x] in R |_2 A )
assume that
A5: ( x in A & y in A ) and
A6: x <> y ; :: thesis: ( [x,y] in R |_2 A or [y,x] in R |_2 A )
A7: R is_connected_in A by A1;

now :: thesis: ( ( [x,y] in R & [x,y] in R |_2 A ) or ( [y,x] in R & [y,x] in R |_2 A ) )

per cases ( [x,y] in R or [y,x] in R ) by A5, A6, A7;

case A8: [x,y] in R ; :: thesis: [x,y] in R |_2 A

[x,y] in [:A,A:] by A5, ZFMISC_1:87;
hence [x,y] in R |_2 A by A8, XBOOLE_0:def 4; :: thesis: verum

end;

case A9: [y,x] in R ; :: thesis: [y,x] in R |_2 A

[y,x] in [:A,A:] by A5, ZFMISC_1:87;
hence [y,x] in R |_2 A by A9, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence ( [x,y] in R |_2 A or [y,x] in R |_2 A ) ; :: thesis: verum

end;

A10: R |_2 A c= R by XBOOLE_1:17;
A11: R |_2 A is_antisymmetric_in A

proof

let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in A or not y in A or not [x,y] in R |_2 A or not [y,x] in R |_2 A or x = y )
assume A12: ( x in A & y in A & [x,y] in R |_2 A & [y,x] in R |_2 A ) ; :: thesis: x = y
R is_antisymmetric_in A by A1;
hence x = y by A10, A12; :: thesis: verum

end;

A13: R |_2 A is_well_founded_in A

proof

let Y be set ; :: according to WELLORD1:def 3 :: thesis: ( not Y c= A or Y = {} or ex b₁ being object st
( b₁ in Y & (R |_2 A) -Seg b₁ misses Y ) )
assume A14: ( Y c= A & Y <> {} ) ; :: thesis: ex b₁ being object st
( b₁ in Y & (R |_2 A) -Seg b₁ misses Y )
R is_well_founded_in A by A1;
then consider a being object such that
A15: ( a in Y & R -Seg a misses Y ) by A14;
(R |_2 A) -Seg a c= R -Seg a by WELLORD1:14;
hence ex b₁ being object st
( b₁ in Y & (R |_2 A) -Seg b₁ misses Y ) by A15, XBOOLE_1:63; :: thesis: verum

end;

A16: A c= field (R |_2 A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in field (R |_2 A) )
assume x in A ; :: thesis: x in field (R |_2 A)
then ( [x,x] in [:A,A:] & [x,x] in R ) by A2, ZFMISC_1:87;
then [x,x] in R |_2 A by XBOOLE_0:def 4;
hence x in field (R |_2 A) by RELAT_1:15; :: thesis: verum

end;

A17: R |_2 A is_transitive_in A

proof

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in A or not y in A or not z in A or not [x,y] in R |_2 A or not [y,z] in R |_2 A or [x,z] in R |_2 A )
assume that
A18: x in A and
A19: y in A and
A20: z in A and
A21: ( [x,y] in R |_2 A & [y,z] in R |_2 A ) ; :: thesis: [x,z] in R |_2 A
A22: [x,z] in [:A,A:] by A18, A20, ZFMISC_1:87;
R is_transitive_in A by A1;
then [x,z] in R by A10, A18, A19, A20, A21;
hence [x,z] in R |_2 A by A22, XBOOLE_0:def 4; :: thesis: verum

end;

field (R |_2 A) c= A by WELLORD1:13;
hence ( R |_2 A well_orders A & A = field (R |_2 A) ) by A16, A3, A17, A11, A4, A13; :: thesis: verum