for x, W being set st x in card (Tarski-Class W) holds
x in Tarski-Class W by Th13;