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