let m be Cardinal; :: thesis: for W being set st W is Tarski & m in card W holds
m in W
let W be set ; :: thesis: ( W is Tarski & m in card W implies m in W )
assume A1: W is Tarski ; :: thesis: ( not m in card W or m in W )
assume m in card W ; :: thesis: m in W
then m in On W by A1, Th9;
hence m in W by ORDINAL1:def 9; :: thesis: verum