TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) is SubSpace of TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) by TSEP_1:2;
then reconsider T = TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) as SubSpace of TOP-REAL n by PRE_TOPC:65;
take T ; :: thesis: ( T is strict & not T is empty & T is convex )
thus ( T is strict & not T is empty ) ; :: thesis: T is convex
[#] (TOP-REAL n) = [#] TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) ;
hence [#] T is convex Subset of (TOP-REAL n) by JORDAN2C:21; :: according to TOPALG_2:def 1 :: thesis: verum