reconsider T = R^1 as non empty strict SubSpace of R^1 by TSEP_1:2;
take T ; :: thesis: ( T is strict & not T is empty & T is interval )
thus ( T is strict & not T is empty & T is interval ) by Lm7; :: thesis: verum