for W being set st W is Tarski & W is epsilon-transitive holds
Rank (card W) = W by Th27, Th30;