let Y, Z 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, b be object ; :: according to RELAT_1:def 2 :: 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 ;
hence [a,b] in R |_2 Z by ; :: 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 ;
then ( a in Z & b in Z ) by ZFMISC_1:87;
then [a,b] in [:Y,Y:] by ;
then [a,b] in R |_2 Y by ;
hence [a,b] in (R |_2 Y) |_2 Z by ; :: thesis: verum