let Z, Y be set ; :: thesis: for R being Relation st Z c= Y holds
(R |_2 Y) |_2 Z = R |_2 Z
let R be Relation; :: thesis: ( Z c= Y implies (R |_2 Y) |_2 Z = R |_2 Z )
assume A1: Z c= Y ; :: thesis: (R |_2 Y) |_2 Z = R |_2 Z
let a be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( 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 ) )
let b be set ; :: thesis: ( ( 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 ) :: thesis: ( not [a,b] in R |_2 Z or [a,b] in (R |_2 Y) |_2 Z )

proof

assume A2: [a,b] in (R |_2 Y) |_2 Z ; :: thesis: [a,b] in R |_2 Z
then [a,b] in R |_2 Y by XBOOLE_0:def 4;
then A3: [a,b] in R by XBOOLE_0:def 4;
[a,b] in [:Z,Z:] by A2, XBOOLE_0:def 4;
hence [a,b] in R |_2 Z by A3, XBOOLE_0:def 4; :: thesis: verum

end;

assume A4: [a,b] in R |_2 Z ; :: thesis: [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; :: thesis: verum