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 )
thus ( [#] (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, NAT_1:14; :: thesis: verum