let R, R1, R2 be Relation; :: thesis: (R \, R1) \, R2 = R \, (R1 \, R2)
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in (R \, R1) \, R2 or [x,y] in R \, (R1 \, R2) ) & ( not [x,y] in R \, (R1 \, R2) or [x,y] in (R \, R1) \, R2 ) )
reconsider xx = x, yy = y as set by TARSKI:1;
thus ( [x,y] in (R \, R1) \, R2 implies [x,y] in R \, (R1 \, R2) ) :: thesis: ( not [x,y] in R \, (R1 \, R2) or [x,y] in (R \, R1) \, R2 )

proof

assume [x,y] in (R \, R1) \, R2 ; :: thesis: [x,y] in R \, (R1 \, R2)
then xx,yy in (R \, R1) \, R2 ;
then ( xx,yy in R \, R1 or ( yy,xx nin R \, R1 & xx,yy in R2 ) ) by Th9;
then ( xx,yy in R or ( yy,xx nin R & xx,yy in R1 ) or ( yy,xx nin R & ( xx,yy in R or yy,xx nin R1 ) & xx,yy in R2 ) ) by Th9;
then ( xx,yy in R or ( yy,xx nin R & xx,yy in R1 \, R2 ) ) by Th9;
then xx,yy in R \, (R1 \, R2) by Th9;
hence [x,y] in R \, (R1 \, R2) ; :: thesis: verum

end;

assume [x,y] in R \, (R1 \, R2) ; :: thesis: [x,y] in (R \, R1) \, R2
then xx,yy in R \, (R1 \, R2) ;
then ( xx,yy in R or ( yy,xx nin R & xx,yy in R1 \, R2 ) ) by Th9;
then ( xx,yy in R or ( yy,xx nin R & ( xx,yy in R1 or ( yy,xx nin R1 & xx,yy in R2 ) ) ) ) by Th9;
then ( xx,yy in R \, R1 or ( yy,xx nin R \, R1 & xx,yy in R2 ) ) by Th9;
then xx,yy in (R \, R1) \, R2 by Th9;
hence [x,y] in (R \, R1) \, R2 ; :: thesis: verum