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