let V be RealLinearSpace; :: thesis: for w1, w2 being VECTOR of V holds w1 in Z_Lin {w1,w2}
let w1, w2 be VECTOR of V; :: thesis: w1 in Z_Lin {w1,w2}
w1 in {w1,w2} by TARSKI:def 2;
hence w1 in Z_Lin {w1,w2} by Th12; :: thesis: verum