let k, n be natural Number ; :: thesis: ( k in Segm n iff k < n )

hereby :: thesis: ( k < n implies k in Segm n )

assume k in Segm n ; :: thesis: k < n
then k in { l where l is Nat : l < n } by AXIOMS:4;
then ex l being Nat st
( k = l & l < n ) ;
hence k < n ; :: thesis: verum

end;

assume A1: k < n ; :: thesis: k in Segm n
reconsider k = k as Element of NAT by ORDINAL1:def 12;
k in { l where l is Nat : l < n } by A1;
hence k in Segm n by AXIOMS:4; :: thesis: verum