let m, n be Nat; :: thesis: ( 2 * (m + 1) <= n implies card (Domin_0 (n,(m + 1))) = (n choose (m + 1)) - (n choose m) )
set CH = Choose (n,(m + 1),1,0);
set Z = Domin_0 (n,(m + 1));
set W = Choose (n,m,1,0);
A1: ( card (Choose (n,(m + 1),1,0)) = (card n) choose (m + 1) & card n = n ) by CARD_FIN:16;
card ((Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1)))) = (card (Choose (n,(m + 1),1,0))) - (card (Domin_0 (n,(m + 1)))) by Th21, CARD_2:44;
then A2: card (Domin_0 (n,(m + 1))) = (card (Choose (n,(m + 1),1,0))) - (card ((Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1))))) ;
assume 2 * (m + 1) <= n ; :: thesis: card (Domin_0 (n,(m + 1))) = (n choose (m + 1)) - (n choose m)
then card (Domin_0 (n,(m + 1))) = (card (Choose (n,(m + 1),1,0))) - (card (Choose (n,m,1,0))) by A2, Th27;
hence card (Domin_0 (n,(m + 1))) = (n choose (m + 1)) - (n choose m) by A1, CARD_FIN:16; :: thesis: verum