let x, y be object ; :: according to ZFMISC_1:def 10 :: thesis: ( not x in dom R or not y in dom R or x = y )
assume x in dom R ; :: thesis: ( not y in dom R or x = y )
then consider a being object such that
A1: [x,a] in R by XTUPLE_0:def 12;
assume y in dom R ; :: thesis: x = y
then consider b being object such that
A2: [y,b] in R by XTUPLE_0:def 12;
[x,a] = [y,b] by A1, A2, ZFMISC_1:def 10;
hence x = y by XTUPLE_0:1; :: thesis: verum