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