now :: thesis: for V1 being Subset of V st V1 is additively-linearly-closed holds
V1 is additively-closed

let V1 be Subset of V; :: 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 V st b₁ is additively-linearly-closed holds
b₁ is additively-closed ; :: thesis: verum