let R be Relation; :: thesis: for X being Subset of (field R) st R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X holds
for s being Sequence of field R st rng s = X & s is increasing holds
s is_isomorphism_of RelIncl (dom s),R |_2 X
let X be Subset of (field R); :: thesis: ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X implies for s being Sequence of field R st rng s = X & s is increasing holds
s is_isomorphism_of RelIncl (dom s),R |_2 X )
set R2 = R |_2 X;
assume A1: ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X ) ; :: thesis: for s being Sequence of field R st rng s = X & s is increasing holds
s is_isomorphism_of RelIncl (dom s),R |_2 X
A2: 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 A1, RELAT_2:def 1;
hence a in field (R |_2 X) by RELAT_1:15; :: thesis: verum

end;

let s be Sequence of field R; :: thesis: ( rng s = X & s is increasing implies s is_isomorphism_of RelIncl (dom s),R |_2 X )
assume A3: ( rng s = X & s is increasing ) ; :: thesis: s is_isomorphism_of RelIncl (dom s),R |_2 X
set O = dom s;
set RO = RelIncl (dom s);
A4: field (RelIncl (dom s)) = dom s by WELLORD2:def 1;
A5: dom s = field (RelIncl (dom s)) by WELLORD2:def 1;
A6: rng s = field (R |_2 X) by A3, A2, WELLORD1:13;
for a, b being object holds
( [a,b] in RelIncl (dom s) iff ( a in field (RelIncl (dom s)) & b in field (RelIncl (dom s)) & [(s . a),(s . b)] in R |_2 X ) )

proof

let a, b be object ; :: thesis: ( [a,b] in RelIncl (dom s) iff ( a in field (RelIncl (dom s)) & b in field (RelIncl (dom s)) & [(s . a),(s . b)] in R |_2 X ) )
thus ( [a,b] in RelIncl (dom s) implies ( a in field (RelIncl (dom s)) & b in field (RelIncl (dom s)) & [(s . a),(s . b)] in R |_2 X ) ) :: thesis: ( a in field (RelIncl (dom s)) & b in field (RelIncl (dom s)) & [(s . a),(s . b)] in R |_2 X implies [a,b] in RelIncl (dom s) )

proof

assume A7: [a,b] in RelIncl (dom s) ; :: thesis: ( a in field (RelIncl (dom s)) & b in field (RelIncl (dom s)) & [(s . a),(s . b)] in R |_2 X )
hence A8: ( a in field (RelIncl (dom s)) & b in field (RelIncl (dom s)) ) by RELAT_1:15; :: thesis: [(s . a),(s . b)] in R |_2 X
reconsider a = a, b = b as Ordinal by A8, A4;

per cases ( a = b or a c< b ) by A8, A7, A4, WELLORD2:def 1;

suppose A9: a = b ; :: thesis: [(s . a),(s . b)] in R |_2 X

s . a in rng s by A5, A8, FUNCT_1:def 3;
hence [(s . a),(s . b)] in R |_2 X by A9, A3, A1, RELAT_2:def 1; :: thesis: verum

end;

suppose a c< b ; :: thesis: [(s . a),(s . b)] in R |_2 X

then a in b by ORDINAL1:11;
then A10: [(s . a),(s . b)] in R by A3, A5, A8;
( s . a in rng s & s . b in rng s ) by A5, A8, FUNCT_1:def 3;
then [(s . a),(s . b)] in [:X,X:] by A3, ZFMISC_1:87;
then [(s . a),(s . b)] in R /\ [:X,X:] by A10, XBOOLE_0:def 4;
hence [(s . a),(s . b)] in R |_2 X by WELLORD1:def 6; :: thesis: verum

end;

end;

end;

assume A11: ( a in field (RelIncl (dom s)) & b in field (RelIncl (dom s)) & [(s . a),(s . b)] in R |_2 X & not [a,b] in RelIncl (dom s) ) ; :: thesis: contradiction
then reconsider a = a, b = b as Ordinal by A4;
not a c= b by A11, A5, WELLORD2:def 1;
then b in a by ORDINAL1:16;
then A12: ( s . b <> s . a & [(s . b),(s . a)] in R ) by A3, A11, A5;
A13: ( s . a in X & s . b in X ) by A3, A11, A5, FUNCT_1:def 3;
then [(s . b),(s . a)] in [:X,X:] by ZFMISC_1:87;
then [(s . b),(s . a)] in R /\ [:X,X:] by A12, XBOOLE_0:def 4;
then [(s . b),(s . a)] in R |_2 X by WELLORD1:def 6;
hence contradiction by A12, A11, A13, A1, RELAT_2:def 4; :: thesis: verum

end;

hence s is_isomorphism_of RelIncl (dom s),R |_2 X by A5, A6, A3, WELLORD1:def 7; :: thesis: verum