let k, n be Nat; :: thesis: ( k in Segm n implies ( k <= n - 1 & n - 1 is Element of NAT ) )

assume k in Segm n ; :: thesis: ( k <= n - 1 & n - 1 is Element of NAT )

then k in { l where l is Nat : l < n } by AXIOMS:4;

then A1: ex l being Nat st

( k = l & l < n ) ;

then A2: n - 1 is Element of NAT by NAT_1:20;

k < (n - 1) + 1 by A1;

hence ( k <= n - 1 & n - 1 is Element of NAT ) by A2, NAT_1:13; :: thesis: verum

assume k in Segm n ; :: thesis: ( k <= n - 1 & n - 1 is Element of NAT )

then k in { l where l is Nat : l < n } by AXIOMS:4;

then A1: ex l being Nat st

( k = l & l < n ) ;

then A2: n - 1 is Element of NAT by NAT_1:20;

k < (n - 1) + 1 by A1;

hence ( k <= n - 1 & n - 1 is Element of NAT ) by A2, NAT_1:13; :: thesis: verum