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