let A be Ordinal; :: thesis: succ A c= bool A
let x be object ; :: 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 reconsider B = x as Ordinal ;
( x in A or x = A ) by A1, ORDINAL1:8;
then B c= A by ORDINAL1:def 2;
hence x in bool A ; :: thesis: verum