now

let V1 be Subset of ; :: thesis: ( V1 is additively-linearly-closed implies V1 is additively-closed )
assume V1 is additively-linearly-closed ; :: thesis: V1 is additively-closed
then ( V1 is add-closed & V1 is having-inverse ) by Def10;
hence V1 is additively-closed ; :: thesis: verum

end;

hence for b₁ being Subset of st b₁ is additively-linearly-closed holds
b₁ is additively-closed ; :: thesis: verum