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