:: deftheorem Def1 defines multi-closed LPSPACC1:def 1 :
for V being non empty CLSStruct
for V1 being Subset of V holds
( V1 is multi-closed iff for a being Complex
for v being VECTOR of V st v in V1 holds
a * v in V1 );