theorem Th6: :: REAL_NS2:6

for n being Nat holds 0. (TOP-REAL n) = 0. (REAL-NS n)