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