let V be RealLinearSpace; :: thesis: for V1 being Subset of V holds
( V1 is linearly-closed iff ( V1 is add-closed & V1 is multi-closed ) )
let V1 be Subset of V; :: thesis: ( V1 is linearly-closed iff ( V1 is add-closed & V1 is multi-closed ) )

hereby :: thesis: ( V1 is add-closed & V1 is multi-closed implies V1 is linearly-closed )

assume V1 is linearly-closed ; :: thesis: ( V1 is add-closed & V1 is multi-closed )
then ( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1 ) ) by RLSUB_1:def 1;
hence ( V1 is add-closed & V1 is multi-closed ) by RLSUBDef0, IDEAL_1:def 1; :: thesis: verum

end;

assume ( V1 is add-closed & V1 is multi-closed ) ; :: thesis: V1 is linearly-closed
then ( ( for v, u being Element of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1 ) ) by RLSUBDef0, IDEAL_1:def 1;
hence V1 is linearly-closed by RLSUB_1:def 1; :: thesis: verum