let s be Real; :: thesis: ( s > 0 implies ex n being Element of NAT st
( n > 0 & 0 < 1 / n & 1 / n <= s ) )
consider n being Nat such that
A1: n > 1 / s by SEQ_4:3;
A2: 1 / (1 / s) = 1 / (s ")
.= s ;
A3: n in NAT by ORDINAL1:def 12;
assume s > 0 ; :: thesis: ex n being Element of NAT st
( n > 0 & 0 < 1 / n & 1 / n <= s )
then A4: 1 / s > 0 ;
take n ; :: thesis: ( n is Element of NAT & n > 0 & 0 < 1 / n & 1 / n <= s )
thus ( n is Element of NAT & n > 0 & 0 < 1 / n & 1 / n <= s ) by A4, A1, A2, XREAL_1:85, A3; :: thesis: verum