let W, x be set ; :: thesis: ( W is Tarski & x in card W implies x in W )
assume A1: W is Tarski ; :: thesis: ( not x in card W or x in W )
assume x in card W ; :: thesis: x in W
then x in On W by A1, Th10;
hence x in W by ORDINAL1:def 10; :: thesis: verum