let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V st L is circled holds
L <> ZeroLC V
let L be Linear_Combination of V; :: thesis: ( L is circled implies L <> ZeroLC V )
assume that
A1: L is circled and
A2: L = ZeroLC V ; :: thesis: contradiction
Carrier L <> {} by A1, Th16;
hence contradiction by A2, RLVECT_2:def 7; :: thesis: verum