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 )

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

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

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