let k be Element of NAT ; :: thesis: for X being non empty finite Subset of [:NAT ,{k}:] ex n being non empty Element of NAT st X c= [:((Seg n) \/ {0 }),{k}:]
let X be non empty finite Subset of [:NAT ,{k}:]; :: thesis: ex n being non empty Element of NAT st X c= [:((Seg n) \/ {0 }),{k}:]
reconsider pX = proj1 X as non empty finite Subset of NAT by FUNCT_5:13;
reconsider mpX = max pX as Element of NAT by ORDINAL1:def 13;
reconsider m = mpX + 1 as non empty Element of NAT ;
take m ; :: thesis: X c= [:((Seg m) \/ {0 }),{k}:]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in [:((Seg m) \/ {0 }),{k}:] )
assume A1: x in X ; :: thesis: x in [:((Seg m) \/ {0 }),{k}:]
then consider x1, x2 being set such that
A2: ( x1 in NAT & x2 in {k} & x = [x1,x2] ) by ZFMISC_1:def 2;
A3: x1 = x `1 by A2, MCART_1:7;
reconsider n = x `1 as Element of NAT by A2, MCART_1:7;
A4: ( Seg m c= (Seg m) \/ {0 } & {0 } c= (Seg m) \/ {0 } ) by XBOOLE_1:7;
A5: max pX <= m by NAT_1:11;
n in pX by A1, A2, A3, RELAT_1:def 4;
then n <= max pX by XXREAL_2:def 8;
then A6: n <= m by A5, XXREAL_0:2;

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

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

then n in Seg m by A6, FINSEQ_1:3;
hence x in [:((Seg m) \/ {0 }),{k}:] by A2, A3, A4, ZFMISC_1:106; :: thesis: verum

end;

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

then n in {0 } by TARSKI:def 1;
hence x in [:((Seg m) \/ {0 }),{k}:] by A2, A3, A4, ZFMISC_1:106; :: thesis: verum

end;

end;