let X, Y, Z be set ; :: thesis: for R being Relation holds
( ( R c= [:X,Y:] & Z c= X implies R | Z = R /\ [:Z,Y:] ) & ( R c= [:X,Y:] implies Z | R = R /\ [:X,Z:] ) )
let R be Relation; :: thesis: ( ( R c= [:X,Y:] & Z c= X implies R | Z = R /\ [:Z,Y:] ) & ( R c= [:X,Y:] implies Z | R = R /\ [:X,Z:] ) )
thus ( R c= [:X,Y:] & Z c= X implies R | Z = R /\ [:Z,Y:] ) :: thesis: ( R c= [:X,Y:] implies Z | R = R /\ [:X,Z:] )

proof

assume that
A1: R c= [:X,Y:] and
Z c= X ; :: thesis: R | Z = R /\ [:Z,Y:]
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in R | Z or [x,b₁] in R /\ [:Z,Y:] ) & ( not [x,b₁] in R /\ [:Z,Y:] or [x,b₁] in R | Z ) )
let y be set ; :: thesis: ( ( not [x,y] in R | Z or [x,y] in R /\ [:Z,Y:] ) & ( not [x,y] in R /\ [:Z,Y:] or [x,y] in R | Z ) )
thus ( [x,y] in R | Z implies [x,y] in R /\ [:Z,Y:] ) :: thesis: ( not [x,y] in R /\ [:Z,Y:] or [x,y] in R | Z )

proof

assume A2: [x,y] in R | Z ; :: thesis: [x,y] in R /\ [:Z,Y:]
then A3: x in Z by RELAT_1:def 11;
A4: [x,y] in R by A2, RELAT_1:def 11;
then y in Y by A1, ZFMISC_1:106;
then [x,y] in [:Z,Y:] by A3, ZFMISC_1:106;
hence [x,y] in R /\ [:Z,Y:] by A4, XBOOLE_0:def 4; :: thesis: verum

end;

thus ( [x,y] in R /\ [:Z,Y:] implies [x,y] in R | Z ) :: thesis: verum

proof

assume A5: [x,y] in R /\ [:Z,Y:] ; :: thesis: [x,y] in R | Z
then [x,y] in [:Z,Y:] by XBOOLE_0:def 4;
then A6: x in Z by ZFMISC_1:106;
[x,y] in R by A5, XBOOLE_0:def 4;
hence [x,y] in R | Z by A6, RELAT_1:def 11; :: thesis: verum

end;

end;

assume A7: R c= [:X,Y:] ; :: thesis: Z | R = R /\ [:X,Z:]
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in Z | R or [x,b₁] in R /\ [:X,Z:] ) & ( not [x,b₁] in R /\ [:X,Z:] or [x,b₁] in Z | R ) )
let y be set ; :: thesis: ( ( not [x,y] in Z | R or [x,y] in R /\ [:X,Z:] ) & ( not [x,y] in R /\ [:X,Z:] or [x,y] in Z | R ) )
thus ( [x,y] in Z | R implies [x,y] in R /\ [:X,Z:] ) :: thesis: ( not [x,y] in R /\ [:X,Z:] or [x,y] in Z | R )

proof

assume A8: [x,y] in Z | R ; :: thesis: [x,y] in R /\ [:X,Z:]
then A9: y in Z by RELAT_1:def 12;
A10: [x,y] in R by A8, RELAT_1:def 12;
then x in X by A7, ZFMISC_1:106;
then [x,y] in [:X,Z:] by A9, ZFMISC_1:106;
hence [x,y] in R /\ [:X,Z:] by A10, XBOOLE_0:def 4; :: thesis: verum

end;

thus ( [x,y] in R /\ [:X,Z:] implies [x,y] in Z | R ) :: thesis: verum

proof

assume A11: [x,y] in R /\ [:X,Z:] ; :: thesis: [x,y] in Z | R
then [x,y] in [:X,Z:] by XBOOLE_0:def 4;
then A12: y in Z by ZFMISC_1:106;
[x,y] in R by A11, XBOOLE_0:def 4;
hence [x,y] in Z | R by A12, RELAT_1:def 12; :: thesis: verum

end;