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