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:] & Z c= 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:] & Z c= 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:] & Z c= Y implies Z | R = R /\ [:X,Z:] )

proof

assume A1: ( R c= [:X,Y:] & 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 [x,y] in R | Z ; :: thesis: [x,y] in R /\ [:Z,Y:]
then A2: ( x in Z & [x,y] in R ) by RELAT_1:def 11;
then ( x in Z & y in Y ) by A1, ZFMISC_1:106;
then [x,y] in [:Z,Y:] by ZFMISC_1:106;
hence [x,y] in R /\ [:Z,Y:] by A2, XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

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

end;

end;

assume A3: ( R c= [:X,Y:] & Z c= 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 [x,y] in Z | R ; :: thesis: [x,y] in R /\ [:X,Z:]
then A4: ( y in Z & [x,y] in R ) by RELAT_1:def 12;
then ( y in Z & x in X ) by A3, ZFMISC_1:106;
then [x,y] in [:X,Z:] by ZFMISC_1:106;
hence [x,y] in R /\ [:X,Z:] by A4, XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

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

end;