let N be finite without_zero Subset of NAT; :: thesis: ex k being Nat st N c= Seg k
consider k being Nat such that
A1: for n being Nat st n in N holds
n <= k by STIRL2_1:56;
take k ; :: thesis: N c= Seg k
thus N c= Seg k :: thesis: verum
proof
let x be object ; :: 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 ;
A4: n >= 1 by A2, A3, NAT_1:14;
n <= k by A1, A2, A3;
hence x in Seg k by A3, A4; :: thesis: verum
end;