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

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

hence
R |_2 Y is transitive
by Lm2; :: thesis: verum[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;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