let Y be set ; :: thesis: for R being Relation st R is transitive holds
R |_2 Y is transitive
let R be Relation; :: thesis: ( R is transitive implies R |_2 Y is transitive )
assume A1: R is transitive ; :: thesis: R |_2 Y is transitive

now :: thesis: for a, b, c being object st [a,b] in R |_2 Y & [b,c] in R |_2 Y holds
[a,c] in R |_2 Y

let a, b, c be object ; :: thesis: ( [a,b] in R |_2 Y & [b,c] in R |_2 Y implies [a,c] in R |_2 Y )
assume that
A2: [a,b] in R |_2 Y and
A3: [b,c] in R |_2 Y ; :: thesis: [a,c] in R |_2 Y
( [a,b] in R & [b,c] in R ) by A2, A3, XBOOLE_0:def 4;
then A4: [a,c] in R by A1, Lm2;
[b,c] in [:Y,Y:] by A3, XBOOLE_0:def 4;
then A5: c in Y by ZFMISC_1:87;
[a,b] in [:Y,Y:] by A2, XBOOLE_0:def 4;
then a in Y by ZFMISC_1:87;
then [a,c] in [:Y,Y:] by A5, ZFMISC_1:87;
hence [a,c] in R |_2 Y by A4, XBOOLE_0:def 4; :: thesis: verum

end;

hence R |_2 Y is transitive by Lm2; :: thesis: verum