let x, W 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, Th9;
hence x in W by ORDINAL1:def 9; :: thesis: verum