consider u being Element of W;
{u} is non empty Element of W ;
hence not for b₁ being Element of W holds b₁ is empty ; :: thesis: verum