theorem Th15: :: RLVECT_3:15

for x being object
for V being RealLinearSpace
for A being Subset of V st x in A holds
x in Lin A