theorem :: REAL_NS2:15

for n being Nat
for F being set holds
( F is Subset of (TOP-REAL n) iff F is Subset of (REAL-NS n) ) by Th4;