:: deftheorem defines circledComb CIRCLED1:def 5 :
for V being RealLinearSpace
for b₂ being set holds
( b₂ = circledComb V iff for L being object holds
( L in b₂ iff L is circled_Combination of V ) );