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