let n, m be 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 x in Domin_0 (n,m) ; :: thesis: x in Choose (n,m,1,0)
then consider p being XFinSequence of such that
A1: p = x and
A2: p is dominated_by_0 and
A3: ( dom p = n & Sum p = m ) by Def2;
rng p c= {0,1} by A2, Def1;
hence x in Choose (n,m,1,0) by A1, A3, CARD_FIN:46; :: thesis: verum