let R be Relation; :: thesis: for X being set st R is_transitive_in X holds
R |_2 X is transitive
let X be set ; :: thesis: ( R is_transitive_in X implies R |_2 X is transitive )
assume A1: 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 ; :: according to RELAT_2:def 8 :: thesis: R |_2 X is transitive
let x, y, z be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or not z in field (R |_2 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
A2: x in field (R |_2 X) and
A3: y in field (R |_2 X) and
A4: z in field (R |_2 X) ; :: thesis: ( not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X )
A5: z in X by A4, WELLORD1:12;
A6: x in X by A2, WELLORD1:12;
then A7: [x,z] in [:X,X:] by A5, ZFMISC_1:87;
assume that
A8: [x,y] in R |_2 X and
A9: [y,z] in R |_2 X ; :: thesis: [x,z] in R |_2 X
A10: [x,y] in R by A8, XBOOLE_0:def 4;
A11: [y,z] in R by A9, XBOOLE_0:def 4;
y in X by A3, WELLORD1:12;
then [x,z] in R by A1, A6, A5, A10, A11;
hence [x,z] in R |_2 X by A7, XBOOLE_0:def 4; :: thesis: verum