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