let V be RealLinearSpace; :: thesis: for v being VECTOR of V holds v in Lin {v}
let v be VECTOR of V; :: thesis: v in Lin {v}
v in {v} by TARSKI:def 1;
hence v in Lin {v} by RLVECT_3:15; :: thesis: verum