( {} is power-closed & {} is FamUnion-closed ) ;
hence ex b₁ being Grothendieck st b₁ is empty ; :: thesis: verum