let R be Relation; :: thesis: for X being set holds
( ( R |_2 X is transitive implies R is_transitive_in X ) & ( R |_2 X is antisymmetric implies R is_antisymmetric_in X ) )
let X be set ; :: thesis: ( ( R |_2 X is transitive implies R is_transitive_in X ) & ( R |_2 X is antisymmetric implies R is_antisymmetric_in X ) )
set R2 = R |_2 X;
A1: R |_2 X = R /\ [:X,X:] by WELLORD1:def 6;

hereby :: thesis: ( R |_2 X is antisymmetric implies R is_antisymmetric_in X )

assume A2: R |_2 X is transitive ; :: thesis: R is_transitive_in X

now :: thesis: for x, y, z being object st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R

let x, y, z be object ; :: thesis: ( x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R )
assume A3: ( x in X & y in X & z in X & [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then ( [x,y] in [:X,X:] & [y,z] in [:X,X:] ) by ZFMISC_1:87;
then A4: ( [x,y] in R |_2 X & [y,z] in R |_2 X ) by A3, A1, XBOOLE_0:def 4;
then ( x in field (R |_2 X) & y in field (R |_2 X) & z in field (R |_2 X) ) by RELAT_1:15;
then [x,z] in R |_2 X by A4, A2, RELAT_2:def 16, RELAT_2:def 8;
hence [x,z] in R by A1, XBOOLE_0:def 4; :: thesis: verum

end;

hence R is_transitive_in X by RELAT_2:def 8; :: thesis: verum

end;

assume A5: R |_2 X is antisymmetric ; :: thesis: R is_antisymmetric_in X

now :: thesis: for x, y being object st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y

let x, y be object ; :: thesis: ( x in X & y in X & [x,y] in R & [y,x] in R implies x = y )
assume A6: ( x in X & y in X & [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( [x,y] in [:X,X:] & [y,x] in [:X,X:] ) by ZFMISC_1:87;
then A7: ( [x,y] in R |_2 X & [y,x] in R |_2 X ) by A6, A1, XBOOLE_0:def 4;
then ( x in field (R |_2 X) & y in field (R |_2 X) ) by RELAT_1:15;
hence x = y by A7, A5, RELAT_2:def 12, RELAT_2:def 4; :: thesis: verum

end;

hence R is_antisymmetric_in X by RELAT_2:def 4; :: thesis: verum