let X be set ; 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; ( 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
; WELLORD1:def 5 ( field (R |_2 X) = X & R |_2 X is well-ordering )
A6:
R |_2 X is_antisymmetric_in X
A9:
R |_2 X is_well_founded_in X
A15:
R |_2 X is_transitive_in X
proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( 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 )
;
[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;
verum
end;
A21:
R |_2 X is_connected_in X
proof
let x,
y be
object ;
RELAT_2:def 6 ( 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
;
( [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;
verum
end;
thus A25:
field (R |_2 X) = X
R |_2 X is well-ordering
R |_2 X is_reflexive_in X
then
R |_2 X well_orders X
by A15, A6, A21, A9;
hence
R |_2 X is well-ordering
by A25, WELLORD1:4; verum