id {x} = {[x,x]} by SYSREL:13;
hence for b₁ being set st b₁ = (id {x}) \+\ {[x,x]} holds
b₁ is empty ; :: thesis: verum