theorem :: REAL_NS2:16

for n being Nat
for F being set holds
( F is Subset of (REAL-NS n) iff F is Subset of (n -VectSp_over F_Real) ) by Th5;