let A be Ordinal; :: thesis: succ A c= bool A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ A or x in bool A )
assume A1: x in succ A ; :: thesis: x in bool A
then A2: ( x in A or x = A ) by ORDINAL1:13;
reconsider B = x as Ordinal by A1;
B c= A by A2, ORDINAL1:def 2;
hence x in bool A ; :: thesis: verum