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 )

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

thus
( not n block k > 0 or ( 1 <= k & k <= n ) or k = n )
:: thesis: verum
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;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