let A be Ordinal; :: thesis: for W being set st W is Tarski & A in W holds
( succ A in W & A c= W )
let W be set ; :: thesis: ( W is Tarski & A in W implies ( succ A in W & A c= W ) )
assume that
A1: for X, Y being set st X in W & Y c= X holds
Y in W and
A2: for X being set st X in W holds
bool X in W and
for X being set holds
( not X c= W or X,W are_equipotent or X in W ) and
A3: A in W ; :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis: ( succ A in W & A c= W )
bool A in W by A2, A3;
hence succ A in W by A1, ORDINAL2:3; :: thesis: A c= W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in W )
assume A4: x in A ; :: thesis: x in W
then reconsider B = x as Ordinal ;
B c= A by A4, ORDINAL1:def 2;
hence x in W by A1, A3; :: thesis: verum