theorem :: REAL_NS2:60

for n being Nat
for At being Subset of (TOP-REAL n)
for Ar being Subset of (REAL-NS n) st At = Ar holds
Lin At = Lin Ar