0 - 0 = 0 ;
then 0 choose 0 = 1 / (1 * 1) by Def3, Th18
.= 1 ;
hence 0 choose 0 = 1 ; :: thesis: verum