theorem Th3: :: PAPDESAF:3

for V being RealLinearSpace
for x being set holds
( x is Element of (OASpace V) iff x is VECTOR of V )