theorem infin2 (A B: set): $ finite B -> finite (A i^i B) $;
A i^i B C_ B -> finite B -> finite (A i^i B)
A i^i B C_ B
finite B -> finite (A i^i B)