a1: n in NAT by ORDINAL1:def 13;
the carrier of (REAL-US n) = REAL n by Def6
.= the carrier of (TOP-REAL n) by EUCLID:25 ;
hence not REAL-US n is trivial by a1; :: thesis: verum