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 that

A1: R is_reflexive_in X and

A2: R is_transitive_in X and

A3: R is_antisymmetric_in X and

A4: R is_connected_in X and

A5: R is_well_founded_in X ; :: according to WELLORD1:def 5 :: thesis: ( field (R |_2 X) = X & R |_2 X is well-ordering )

A6: R |_2 X is_antisymmetric_in X

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

( 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 that

A1: R is_reflexive_in X and

A2: R is_transitive_in X and

A3: R is_antisymmetric_in X and

A4: R is_connected_in X and

A5: R is_well_founded_in X ; :: according to WELLORD1:def 5 :: thesis: ( field (R |_2 X) = X & R |_2 X is well-ordering )

A6: R |_2 X is_antisymmetric_in X

proof

A9:
R |_2 X is_well_founded_in X
let x, y be object ; :: according to RELAT_2:def 4 :: 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 that

A7: ( x in X & y in X ) and

A8: ( [x,y] in R |_2 X & [y,x] in R |_2 X ) ; :: thesis: x = y

( [x,y] in R & [y,x] in R ) by A8, XBOOLE_0:def 4;

hence x = y by A3, A7; :: thesis: verum

end;assume that

A7: ( x in X & y in X ) and

A8: ( [x,y] in R |_2 X & [y,x] in R |_2 X ) ; :: thesis: x = y

( [x,y] in R & [y,x] in R ) by A8, XBOOLE_0:def 4;

hence x = y by A3, A7; :: thesis: verum

proof

A15:
R |_2 X is_transitive_in X
let Y be set ; :: according to WELLORD1:def 3 :: thesis: ( not Y c= X or Y = {} or ex b_{1} being object st

( b_{1} in Y & (R |_2 X) -Seg b_{1} misses Y ) )

assume ( Y c= X & Y <> {} ) ; :: thesis: ex b_{1} being object st

( b_{1} in Y & (R |_2 X) -Seg b_{1} misses Y )

then consider a being object such that

A10: a in Y and

A11: R -Seg a misses Y by A5;

take a ; :: thesis: ( a in Y & (R |_2 X) -Seg a misses Y )

thus a in Y by A10; :: thesis: (R |_2 X) -Seg a misses Y

assume not (R |_2 X) -Seg a misses Y ; :: thesis: contradiction

then consider x being object such that

A12: x in (R |_2 X) -Seg a and

A13: x in Y by XBOOLE_0:3;

[x,a] in R |_2 X by A12, WELLORD1:1;

then A14: [x,a] in R by XBOOLE_0:def 4;

x <> a by A12, WELLORD1:1;

then x in R -Seg a by A14, WELLORD1:1;

hence contradiction by A11, A13, XBOOLE_0:3; :: thesis: verum

end;( b

assume ( Y c= X & Y <> {} ) ; :: thesis: ex b

( b

then consider a being object such that

A10: a in Y and

A11: R -Seg a misses Y by A5;

take a ; :: thesis: ( a in Y & (R |_2 X) -Seg a misses Y )

thus a in Y by A10; :: thesis: (R |_2 X) -Seg a misses Y

assume not (R |_2 X) -Seg a misses Y ; :: thesis: contradiction

then consider x being object such that

A12: x in (R |_2 X) -Seg a and

A13: x in Y by XBOOLE_0:3;

[x,a] in R |_2 X by A12, WELLORD1:1;

then A14: [x,a] in R by XBOOLE_0:def 4;

x <> a by A12, WELLORD1:1;

then x in R -Seg a by A14, WELLORD1:1;

hence contradiction by A11, A13, XBOOLE_0:3; :: thesis: verum

proof

A21:
R |_2 X is_connected_in X
let x, y, z be object ; :: according to RELAT_2:def 8 :: 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 that

A16: x in X and

A17: y in X and

A18: z in X and

A19: ( [x,y] in R |_2 X & [y,z] in R |_2 X ) ; :: thesis: [x,z] in R |_2 X

( [x,y] in R & [y,z] in R ) by A19, XBOOLE_0:def 4;

then A20: [x,z] in R by A2, A16, A17, A18;

[x,z] in [:X,X:] by A16, A18, ZFMISC_1:87;

hence [x,z] in R |_2 X by A20, XBOOLE_0:def 4; :: thesis: verum

end;assume that

A16: x in X and

A17: y in X and

A18: z in X and

A19: ( [x,y] in R |_2 X & [y,z] in R |_2 X ) ; :: thesis: [x,z] in R |_2 X

( [x,y] in R & [y,z] in R ) by A19, XBOOLE_0:def 4;

then A20: [x,z] in R by A2, A16, A17, A18;

[x,z] in [:X,X:] by A16, A18, ZFMISC_1:87;

hence [x,z] in R |_2 X by A20, XBOOLE_0:def 4; :: thesis: verum

proof

thus A25:
field (R |_2 X) = X
:: thesis: R |_2 X is well-ordering
let x, y be object ; :: according to RELAT_2:def 6 :: 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 that

A22: ( x in X & y in X ) and

A23: x <> y ; :: thesis: ( [x,y] in R |_2 X or [y,x] in R |_2 X )

A24: ( [x,y] in [:X,X:] & [y,x] in [:X,X:] ) by A22, ZFMISC_1:87;

( [x,y] in R or [y,x] in R ) by A4, A22, A23;

hence ( [x,y] in R |_2 X or [y,x] in R |_2 X ) by A24, XBOOLE_0:def 4; :: thesis: verum

end;assume that

A22: ( x in X & y in X ) and

A23: x <> y ; :: thesis: ( [x,y] in R |_2 X or [y,x] in R |_2 X )

A24: ( [x,y] in [:X,X:] & [y,x] in [:X,X:] ) by A22, ZFMISC_1:87;

( [x,y] in R or [y,x] in R ) by A4, A22, A23;

hence ( [x,y] in R |_2 X or [y,x] in R |_2 X ) by A24, XBOOLE_0:def 4; :: thesis: verum

proof

R |_2 X is_reflexive_in X
thus
field (R |_2 X) c= X
by WELLORD1:13; :: according to XBOOLE_0:def 10 :: thesis: X c= field (R |_2 X)

let x be object ; :: 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, ZFMISC_1:87;

then [x,x] in R |_2 X by XBOOLE_0:def 4;

hence x in field (R |_2 X) by RELAT_1:15; :: thesis: verum

end;let x be object ; :: 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, ZFMISC_1:87;

then [x,x] in R |_2 X by XBOOLE_0:def 4;

hence x in field (R |_2 X) by RELAT_1:15; :: thesis: verum

proof

then
R |_2 X well_orders X
by A15, A6, A21, A9;
let x be object ; :: 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, ZFMISC_1:87;

hence [x,x] in R |_2 X by XBOOLE_0:def 4; :: thesis: verum

end;assume x in X ; :: thesis: [x,x] in R |_2 X

then ( [x,x] in R & [x,x] in [:X,X:] ) by A1, ZFMISC_1:87;

hence [x,x] in R |_2 X by XBOOLE_0:def 4; :: thesis: verum

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