let n, m be Element of NAT ; :: thesis: Domin_0 n,m c= Choose n,m,1,0
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Domin_0 n,m or x in Choose n,m,1,0 )
assume A1: x in Domin_0 n,m ; :: thesis: x in Choose n,m,1,0
consider p being XFinSequence of such that
A2: ( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) by A1, Def2;
rng p c= {0 ,1} by A2, Def1;
hence x in Choose n,m,1,0 by A2, CARD_FIN:46; :: thesis: verum