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

( 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