(TOP-REAL (n + 1)) | (Sphere ((0. (TOP-REAL (n + 1))),1)) is second-countable ;
then Tcircle ((0. (TOP-REAL (n + 1))),1) is second-countable by TOPREALB:def 6;
hence TUnitSphere n is second-countable by TOPREALB:def 7; :: thesis: verum