{} in sproduct the Object-Kind of S by CARD_3:66;
hence ex b₁ being Element of sproduct the Object-Kind of S st b₁ is finite ; :: thesis: verum