let V be RealUnitarySpace; :: thesis: 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; :: thesis: ( 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, Th2; :: thesis: verum