:: deftheorem defines LC_CLSpace CONVEX4:def 17 :
for V being non empty CLSStruct holds LC_CLSpace V = CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #);