let X be set ; :: thesis: for R being Relation st R well_orders X holds
( field (R |_2 X) = X & R |_2 X is well-ordering )
let R be Relation; :: thesis: ( R well_orders X implies ( field (R |_2 X) = X & R |_2 X is well-ordering ) )
assume A1: ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X ) ; :: according to WELLORD1:def 5 :: thesis: ( field (R |_2 X) = X & R |_2 X is well-ordering )
thus A2: field (R |_2 X) = X :: thesis: R |_2 X is well-ordering

proof

thus field (R |_2 X) c= X by WELLORD1:20; :: according to XBOOLE_0:def 10 :: thesis: X c= field (R |_2 X)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in field (R |_2 X) )
assume x in X ; :: thesis: x in field (R |_2 X)
then ( [x,x] in R & [x,x] in [:X,X:] ) by A1, RELAT_2:def 1, ZFMISC_1:106;
then [x,x] in R |_2 X by XBOOLE_0:def 4;
hence x in field (R |_2 X) by RELAT_1:30; :: thesis: verum

end;

R |_2 X well_orders X

proof

thus R |_2 X is_reflexive_in X :: according to WELLORD1:def 5 :: thesis: ( R |_2 X is_transitive_in X & R |_2 X is_antisymmetric_in X & R |_2 X is_connected_in X & R |_2 X is_well_founded_in X )

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in R |_2 X )
assume x in X ; :: thesis: [x,x] in R |_2 X
then ( [x,x] in R & [x,x] in [:X,X:] ) by A1, RELAT_2:def 1, ZFMISC_1:106;
hence [x,x] in R |_2 X by XBOOLE_0:def 4; :: thesis: verum

end;

thus R |_2 X is_transitive_in X :: thesis: ( R |_2 X is_antisymmetric_in X & R |_2 X is_connected_in X & R |_2 X is_well_founded_in X )

proof

let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in X or not b₁ in X or not b₂ in X or not [x,b₁] in R |_2 X or not [b₁,b₂] in R |_2 X or [x,b₂] in R |_2 X )
let y, z be set ; :: thesis: ( not x in X or not y in X or not z in X or not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X )
assume A3: ( x in X & y in X & z in X & [x,y] in R |_2 X & [y,z] in R |_2 X ) ; :: thesis: [x,z] in R |_2 X
then ( [x,y] in R & [y,z] in R ) by XBOOLE_0:def 4;
then ( [x,z] in R & [x,z] in [:X,X:] ) by A1, A3, RELAT_2:def 8, ZFMISC_1:106;
hence [x,z] in R |_2 X by XBOOLE_0:def 4; :: thesis: verum

end;

thus R |_2 X is_antisymmetric_in X :: thesis: ( R |_2 X is_connected_in X & R |_2 X is_well_founded_in X )

proof

let x be set ; :: according to RELAT_2:def 4 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or not [x,b₁] in R |_2 X or not [b₁,x] in R |_2 X or x = b₁ )
let y be set ; :: thesis: ( not x in X or not y in X or not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y )
assume A4: ( x in X & y in X & [x,y] in R |_2 X & [y,x] in R |_2 X ) ; :: thesis: x = y
then ( [x,y] in R & [y,x] in R ) by XBOOLE_0:def 4;
hence x = y by A1, A4, RELAT_2:def 4; :: thesis: verum

end;

thus R |_2 X is_connected_in X :: thesis: R |_2 X is_well_founded_in X

proof

let x be set ; :: according to RELAT_2:def 6 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or x = b₁ or [x,b₁] in R |_2 X or [b₁,x] in R |_2 X )
let y be set ; :: thesis: ( not x in X or not y in X or x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
assume ( x in X & y in X & x <> y ) ; :: thesis: ( [x,y] in R |_2 X or [y,x] in R |_2 X )
then ( ( [x,y] in R or [y,x] in R ) & [x,y] in [:X,X:] & [y,x] in [:X,X:] ) by A1, RELAT_2:def 6, ZFMISC_1:106;
hence ( [x,y] in R |_2 X or [y,x] in R |_2 X ) by XBOOLE_0:def 4; :: thesis: verum

end;

thus R |_2 X is_well_founded_in X :: thesis: verum

proof

let Y be set ; :: according to WELLORD1:def 3 :: thesis: ( not Y c= X or Y = {} or ex b₁ being set st
( b₁ in Y & (R |_2 X) -Seg b₁ misses Y ) )
assume ( Y c= X & Y <> {} ) ; :: thesis: ex b₁ being set st
( b₁ in Y & (R |_2 X) -Seg b₁ misses Y )
then consider a being set such that
A5: ( a in Y & R -Seg a misses Y ) by A1, WELLORD1:def 3;
take a ; :: thesis: ( a in Y & (R |_2 X) -Seg a misses Y )
thus a in Y by A5; :: thesis: (R |_2 X) -Seg a misses Y
assume not (R |_2 X) -Seg a misses Y ; :: thesis: contradiction
then consider x being set such that
A6: ( x in (R |_2 X) -Seg a & x in Y ) by XBOOLE_0:3;
A7: ( x <> a & [x,a] in R |_2 X ) by A6, WELLORD1:def 1;
then [x,a] in R by XBOOLE_0:def 4;
then x in R -Seg a by A7, WELLORD1:def 1;
hence contradiction by A5, A6, XBOOLE_0:3; :: thesis: verum

end;

end;

hence R |_2 X is well-ordering by A2, WELLORD1:8; :: thesis: verum