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 )
1 <= n by NAT_1:14;
hence ( [#] (TOP-REAL n) is open & [#] (TOP-REAL n) is closed & not [#] (TOP-REAL n) is Bounded & [#] (TOP-REAL n) is convex ) by JORDAN2C:21, JORDAN2C:41; :: thesis: verum