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