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_1:def 5, CARD_FIN:18;
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 Th25, CARD_2:63;
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, Th31;
hence card (Domin_0 n,(m + 1)) = (n choose (m + 1)) - (n choose m) by A1, CARD_FIN:18; :: thesis: verum