let Y, Z be set ; for R being Relation st Z c= Y holds
(R |_2 Y) |_2 Z = R |_2 Z
let R be Relation; ( Z c= Y implies (R |_2 Y) |_2 Z = R |_2 Z )
assume A1:
Z c= Y
; (R |_2 Y) |_2 Z = R |_2 Z
let a, b be object ; RELAT_1:def 2 ( ( not [a,b] in (R |_2 Y) |_2 Z or [a,b] in R |_2 Z ) & ( not [a,b] in R |_2 Z or [a,b] in (R |_2 Y) |_2 Z ) )
thus
( [a,b] in (R |_2 Y) |_2 Z implies [a,b] in R |_2 Z )
( not [a,b] in R |_2 Z or [a,b] in (R |_2 Y) |_2 Z )
assume A4:
[a,b] in R |_2 Z
; [a,b] in (R |_2 Y) |_2 Z
then A5:
[a,b] in R
by XBOOLE_0:def 4;
A6:
[a,b] in [:Z,Z:]
by A4, XBOOLE_0:def 4;
then
( a in Z & b in Z )
by ZFMISC_1:87;
then
[a,b] in [:Y,Y:]
by A1, ZFMISC_1:87;
then
[a,b] in R |_2 Y
by A5, XBOOLE_0:def 4;
hence
[a,b] in (R |_2 Y) |_2 Z
by A6, XBOOLE_0:def 4; verum