let x, y, z be set ; :: according to MMLQUER2:def 1 :: thesis: ( x,y in R1 \, R2 & y,z in R1 \, R2 implies x,z in R1 \, R2 )
assume A1: ( x,y in R1 \, R2 & y,z in R1 \, R2 ) ; :: thesis: x,z in R1 \, R2
then ( [x,y] in R1 \, R2 & [y,z] in R1 \, R2 ) ;
then reconsider x = x, y = y, z = z as Element of X by ZFMISC_1:87;
per cases ( ( x,y in R1 & y,z in R1 ) or ( z,x nin R1 & x,y in R2 & y,z in R2 ) or ( y,x nin R1 & z,y nin R1 & z,x in R1 ) or ( x,y in R1 & z,y nin R1 & y,z in R2 ) or ( y,z in R1 & y,x nin R1 & x,y in R2 ) ) by A1, Th9;
suppose ( ( x,y in R1 & y,z in R1 ) or ( z,x nin R1 & x,y in R2 & y,z in R2 ) ) ; :: thesis: x,z in R1 \, R2
then ( x,z in R1 or ( z,x nin R1 & x,z in R2 ) ) by Def1;
hence x,z in R1 \, R2 by Th9; :: thesis: verum
end;
suppose ( y,x nin R1 & z,y nin R1 & z,x in R1 ) ; :: thesis: x,z in R1 \, R2
hence x,z in R1 \, R2 by Def4; :: thesis: verum
end;
suppose A2: ( x,y in R1 & z,y nin R1 & y,z in R2 ) ; :: thesis: x,z in R1 \, R2
assume not x,z in R1 \, R2 ; :: thesis: contradiction
then x,z nin R1 by Th9;
hence contradiction by A2, Def4; :: thesis: verum
end;
suppose A3: ( y,z in R1 & y,x nin R1 & x,y in R2 ) ; :: thesis: x,z in R1 \, R2
assume not x,z in R1 \, R2 ; :: thesis: contradiction
then x,z nin R1 by Th9;
hence contradiction by A3, Def4; :: thesis: verum
end;
end;