let x be set ; :: according to ZFMISC_1:def 10 :: thesis: for b₁ being set holds
( not x in dom R or not b₁ in dom R or x = b₁ )
let y be set ; :: 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 set such that
A1: [x,a] in R by Def4;
assume y in dom R ; :: thesis: x = y
then consider b being set such that
A2: [y,b] in R by Def4;
[x,a] = [y,b] by A1, A2, ZFMISC_1:def 10;
hence x = y by ZFMISC_1:27; :: thesis: verum