let V be RealLinearSpace; for w1, w2, w3 being VECTOR of V holds
( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )
let w1, w2, w3 be VECTOR of V; ( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )
A1:
w3 in {w1,w2,w3}
by ENUMSET1:def 1;
( w1 in {w1,w2,w3} & w2 in {w1,w2,w3} )
by ENUMSET1:def 1;
hence
( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )
by A1, RLVECT_3:15; verum