let T be SubSpace of R^1 ; :: thesis: ( T = R^1 implies T is interval )
assume A1: T = R^1 ; :: thesis: T is interval
A2: [#] T = REAL by A1, TOPMETR:17;
then reconsider P = [#] T as Subset of REAL ;
P is interval by A2;
hence [#] T is interval ; :: according to TOPALG_2:def 3 :: thesis: verum