for V being RealLinearSpace
for L being Linear_Combination of V st L is circled holds
L <> ZeroLC V by Th16, RLVECT_2:def 5;