set v = the Element of V;
the Element of V is strict AddGroup by Def15;
hence ex b₁ being Element of V st b₁ is strict ; :: thesis: verum