for V being RealLinearSpace
for V1 being Subset of V holds
( V1 is linearly-closed iff ( V1 is add-closed & V1 is multi-closed ) ) by RLSUB_1:def 1;