:: deftheorem defines circledComb CIRCLED1:def 6 :
for V being RealLinearSpace
for M being non empty Subset of V
for b₃ being set holds
( b₃ = circledComb M iff for L being object holds
( L in b₃ iff L is circled_Combination of M ) );