card (p ^^ I) = card I by Th1;
hence p ^^ I is finite ; :: thesis: verum