{((id U) . u)} \ {u} = {} ;
then (id U) . u = u by ZFMISC_1:15;
hence for b₁ being set st b₁ = ((id U) . u) \+\ u holds
b₁ is empty ; :: thesis: verum