for W being set holds Rank (card (Tarski-Class W)) c= Tarski-Class W