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 } )
assume A1: x in X ; :: thesis: x in (Seg m) \/ {0 }
then reconsider n = x as Element of NAT ;
A2: ( Seg m c= (Seg m) \/ {0 } & {0 } c= (Seg m) \/ {0 } ) by XBOOLE_1:7;
A3: n <= m by A1, 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 A3, FINSEQ_1:3;
hence x in (Seg m) \/ {0 } by A2; :: 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;