let k, n be 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

set F = { g where g is Function of (Segm n),(Segm k) : ( g is onto & g is "increasing ) } ;
assume A1: ( ( 1 <= k & k <= n ) or k = n ) ; :: thesis: n block k > 0
( k = 0 iff n = 0 ) by A1;
then consider f being Function of (Segm n),(Segm k) such that
A2: ( f is onto & f is "increasing ) by A1, Th23;
f in { g where g is Function of (Segm n),(Segm k) : ( g is onto & g is "increasing ) } by A2;
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 A3: n block k > 0 ; :: thesis: ( ( 1 <= k & k <= n ) or k = n )
assume A4: ( not ( 1 <= k & k <= n ) & not k = n ) ; :: thesis: contradiction
then ( 1 + 0 > k or k > n ) ;
then ( ( k = 0 & n <> k ) or k > n ) by A4, NAT_1:13;
hence contradiction by A3, Th29, Th31; :: thesis: verum

end;