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