let R be Relation; :: thesis: for X being Subset of (field R) holds
( R well_orders X iff ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X & ex s being Sequence of field R st
( rng s = X & s is increasing ) ) )
let X be Subset of (field R); :: thesis: ( R well_orders X iff ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X & ex s being Sequence of field R st
( rng s = X & s is increasing ) ) )
set R2 = R |_2 X;
thus ( R well_orders X implies ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X & ex s being Sequence of field R st
( rng s = X & s is increasing ) ) ) :: thesis: ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X & ex s being Sequence of field R st
( rng s = X & s is increasing ) implies R well_orders X )

proof

set O = order_type_of (R |_2 X);
set RO = RelIncl (order_type_of (R |_2 X));
assume R well_orders X ; :: thesis: ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X & ex s being Sequence of field R st
( rng s = X & s is increasing ) )
then A1: ( R |_2 X well_orders X & X = field (R |_2 X) ) by PCOMPS_2:1;
then R |_2 X is well-ordering by WELLORD1:4;
then R |_2 X, RelIncl (order_type_of (R |_2 X)) are_isomorphic by WELLORD2:def 2;
then consider f being Function such that
A2: f is_isomorphism_of RelIncl (order_type_of (R |_2 X)),R |_2 X by WELLORD1:40, WELLORD1:def 8;
( field (RelIncl (order_type_of (R |_2 X))) = order_type_of (R |_2 X) & rng f = X ) by A2, A1, WELLORD1:def 7, WELLORD2:def 1;
then A3: ( dom f = order_type_of (R |_2 X) & rng f c= field R ) by A2, WELLORD1:def 7;
then reconsider f = f as Sequence of field R by RELAT_1:def 19, ORDINAL1:def 7;
reconsider f = f as Sequence of field R ;
thus ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X ) by A1, WELLORD1:def 5; :: thesis: ex s being Sequence of field R st
( rng s = X & s is increasing )
take f ; :: thesis: ( rng f = X & f is increasing )
thus rng f = X by A2, A1, WELLORD1:def 7; :: thesis: f is increasing
let A, B be Ordinal; :: according to SURREAL1:def 3 :: thesis: ( A in B & B in dom f implies ( f . A <> f . B & [(f . A),(f . B)] in R ) )
assume A4: ( A in B & B in dom f ) ; :: thesis: ( f . A <> f . B & [(f . A),(f . B)] in R )
A5: A c= B by A4, ORDINAL1:def 2;
A6: A in dom f by A4, ORDINAL1:10;
then [A,B] in RelIncl (order_type_of (R |_2 X)) by A4, A3, A5, WELLORD2:def 1;
then A7: ( [(f . A),(f . B)] in R |_2 X & R |_2 X = R /\ [:X,X:] ) by A2, WELLORD1:def 6, WELLORD1:def 7;
A8: f is one-to-one by A2, WELLORD1:def 7;
A <> B by A4;
hence ( f . A <> f . B & [(f . A),(f . B)] in R ) by A7, A6, A4, A8, FUNCT_1:def 4, XBOOLE_0:def 4; :: thesis: verum

end;

assume A9: ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X ) ; :: thesis: ( for s being Sequence of field R holds
( not rng s = X or not s is increasing ) or R well_orders X )
X c= field (R |_2 X)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in field (R |_2 X) )
assume a in X ; :: thesis: a in field (R |_2 X)
then [a,a] in R |_2 X by A9, RELAT_2:def 1;
hence a in field (R |_2 X) by RELAT_1:15; :: thesis: verum

end;

then A10: X = field (R |_2 X) by WELLORD1:13;
given s being Sequence of field R such that A11: ( rng s = X & s is increasing ) ; :: thesis: R well_orders X
set O = dom s;
set RO = RelIncl (dom s);
A12: s is_isomorphism_of RelIncl (dom s),R |_2 X by A11, Th23, A9;
R |_2 X is well-ordering by A12, WELLORD1:44;
then ( 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 ) by A10, Th21, Th22;
hence R well_orders X by WELLORD1:def 5; :: thesis: verum