(id D) . d = d by FUNCT_1:17;
hence for b₁ being set st b₁ = {((id D) . d)} \ {d} holds
b₁ is empty ; :: thesis: verum