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 13;
take m ; :: thesis: X c= (Seg m) \/ {0 }
let x be set ; :: 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:26;

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

then n in Seg m by A4, FINSEQ_1:3;
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;