consider f being Element of F;
f <> {} ;
hence not for b₁ being Element of F holds b₁ is empty ; :: thesis: verum