x .--> y = {[x,y]} by ZFMISC_1:29;
hence for b₁ being set st b₁ = (x .--> y) \+\ {[x,y]} holds
b₁ is empty ; :: thesis: verum