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

proof

let x, y be object ; :: according to RELAT_1:def 2 :: 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:87;
then [x,y] in [:Z,Y:] by A3, ZFMISC_1:87;
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:87;
[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;

let x, y be object ; :: according to RELAT_1:def 2 :: 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 A7: [x,y] in Z |` R ; :: thesis: [x,y] in R /\ [:X,Z:]
then A8: y in Z by RELAT_1:def 12;
A9: [x,y] in R by A7, RELAT_1:def 12;
then x in X by A1, ZFMISC_1:87;
then [x,y] in [:X,Z:] by A8, ZFMISC_1:87;
hence [x,y] in R /\ [:X,Z:] by A9, XBOOLE_0:def 4; :: thesis: verum

end;

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