let V be a_neighborhood of 0. X; :: according to RLTOPSP1:def 12 :: thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
{} X c= t * V ) )
take s = 1; :: thesis: ( s > 0 & ( for t being Real st t > s holds
{} X c= t * V ) )
thus ( s > 0 & ( for t being Real st t > s holds
{} X c= t * V ) ) by XBOOLE_1:2; :: thesis: verum