let k, n be Element of NAT ; :: thesis: ( ( ( 1 <= k & k <= n ) or k = n ) iff n block k > 0 )
thus ( ( ( 1 <= k & k <= n ) or k = n ) implies n block k > 0 ) :: thesis: ( not n block k > 0 or ( 1 <= k & k <= n ) or k = n )

proof

assume ( ( 1 <= k & k <= n ) or k = n ) ; :: thesis: n block k > 0
then ( ( k = 0 implies n = 0 ) & ( n = 0 implies k = 0 ) & k <= n ) ;
then consider f being Function of n,k such that
A1: ( f is onto & f is "increasing ) by Th23;
set F = { g where g is Function of n,k : ( g is onto & g is "increasing ) } ;
f in { g where g is Function of n,k : ( g is onto & g is "increasing ) } by A1;
hence n block k > 0 ; :: thesis: verum

end;

thus ( not n block k > 0 or ( 1 <= k & k <= n ) or k = n ) :: thesis: verum

proof

assume A2: n block k > 0 ; :: thesis: ( ( 1 <= k & k <= n ) or k = n )
assume ( not ( 1 <= k & k <= n ) & not k = n ) ; :: thesis: contradiction
then ( ( 1 + 0 > k or k > n ) & k <> n ) ;
then ( ( k = 0 & n <> k ) or k > n ) by NAT_1:13;
hence contradiction by A2, Th29, Th31; :: thesis: verum

end;