let Y be set ; for R being Relation st R is transitive holds
R |_2 Y is transitive
let R be Relation; ( R is transitive implies R |_2 Y is transitive )
assume A1:
R is transitive
; R |_2 Y is transitive
now 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 Ylet a,
b,
c be
object ;
( [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
;
[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;
verum end;
hence
R |_2 Y is transitive
by Lm2; verum