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

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

end;

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