let V be RealUnitarySpace; :: thesis: for w1, w2 being VECTOR of V holds
( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
let w1, w2 be VECTOR of V; :: thesis: ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
( w1 in {w1,w2} & w2 in {w1,w2} ) by TARSKI:def 2;
hence ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} ) by Th2; :: thesis: verum