let X be non empty finite Subset of NAT; :: thesis: ex n being Element of NAT st X c= (Seg n) \/ {0}
reconsider m = max X as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis: X c= (Seg m) \/ {0}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (Seg m) \/ {0} )
A1: Seg m c= (Seg m) \/ {0} by XBOOLE_1:7;
A2: {0} c= (Seg m) \/ {0} by XBOOLE_1:7;
assume A3: x in X ; :: thesis: x in (Seg m) \/ {0}
then reconsider n = x as Element of NAT ;
A4: n <= m by A3, XXREAL_2:def 8;

per cases ( 1 <= n or 0 = n ) by NAT_1:25;

suppose 1 <= n ; :: thesis: x in (Seg m) \/ {0}

then n in Seg m by A4, FINSEQ_1:1;
hence x in (Seg m) \/ {0} by A1; :: thesis: verum

end;

suppose 0 = n ; :: thesis: x in (Seg m) \/ {0}

then n in {0} by TARSKI:def 1;
hence x in (Seg m) \/ {0} by A2; :: thesis: verum

end;

end;