let m be Cardinal; :: thesis: for W being set st m in card (Tarski-Class W) holds
m in Tarski-Class W
let W be set ; :: thesis: ( m in card (Tarski-Class W) implies m in Tarski-Class W )
assume m in card (Tarski-Class W) ; :: thesis: m in Tarski-Class W
then m in On (Tarski-Class W) by Th9;
hence m in Tarski-Class W by ORDINAL1:def 9; :: thesis: verum