theorem :: AFINSQ_2:24

for B1, B2 being finite natural-membered set st B1 <N< B2 holds
B1 misses B2