theorem Th12: :: RLVECT_X:12

for x being set
for V being RealLinearSpace
for A being Subset of V st x in A holds
x in Z_Lin A