theorem :: RLVECT_4:34

for V being RealLinearSpace
for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds
( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )