let s be real number ; :: thesis: ( s > 0 implies ex n being Element of NAT st
( n > 0 & 0 < 1 / n & 1 / n <= s ) )
consider n being Element of NAT such that
A1: n > 1 / s by SEQ_4:10;
A2: 1 / (1 / s) = 1 / (s ")
.= s ;
assume s > 0 ; :: thesis: ex n being Element of NAT st
( n > 0 & 0 < 1 / n & 1 / n <= s )
then A3: 1 / s > 0 by XREAL_1:141;
take n ; :: thesis: ( n > 0 & 0 < 1 / n & 1 / n <= s )
n > 0 by A3, A1, XXREAL_0:2;
hence ( n > 0 & 0 < 1 / n & 1 / n <= s ) by A3, A1, A2, XREAL_1:87, XREAL_1:141; :: thesis: verum