let m, n be Nat; :: thesis: Domin_0 (n,m) c= Choose (n,m,1,0)
let x be object ; :: 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 NAT 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;
hence x in Choose (n,m,1,0) by A1, A3, CARD_FIN:40; :: thesis: verum