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 ;
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 ;
hence contradiction by A3, Th29, Th31; :: thesis: verum
end;