for X, W being set st ( ( X in Tarski-Class W & W is epsilon-transitive ) or ( X in Tarski-Class W & X c= Tarski-Class W ) or ( card X in card (Tarski-Class W) & X c= Tarski-Class W ) ) holds
Funcs (X,(Tarski-Class W)) c= Tarski-Class W