A1: n in NAT by ORDINAL1:def 12;
the carrier of (REAL-NS n) = REAL n by Def4
.= the carrier of (TOP-REAL n) by EUCLID:22 ;
hence not REAL-NS n is trivial by A1; :: thesis: verum