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