take [#] (TOP-REAL n) ; :: thesis: ( [#] (TOP-REAL n) is open & [#] (TOP-REAL n) is closed & not [#] (TOP-REAL n) is bounded & [#] (TOP-REAL n) is convex )
reconsider n = n as Element of NAT by ORDINAL1:def 12;
n >= 1 by NAT_1:14;
then not [#] (TOP-REAL n) is bounded by JORDAN2C:35;
hence ( [#] (TOP-REAL n) is open & [#] (TOP-REAL n) is closed & not [#] (TOP-REAL n) is bounded & [#] (TOP-REAL n) is convex ) ; :: thesis: verum