let N be finite without_zero Subset of NAT ; :: thesis: ex k being Nat st N c= Seg k
consider k being Element of NAT such that
A1: for n being Element of NAT st n in N holds
n <= k by STIRL2_1:66;
take k ; :: thesis: N c= Seg k
thus N c= Seg k :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in Seg k )
assume A2: x in N ; :: thesis: x in Seg k
then consider n being Element of NAT such that
A3: n = x ;
( n >= 1 & n <= k ) by A1, A2, A3, NAT_1:14;
hence x in Seg k by A3; :: thesis: verum

end;