consider v being Element of V;
v is strict AddGroup by Def22;
hence ex b₁ being Element of V st b₁ is strict ; :: thesis: verum