let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume A1: S₁[A] ; :: thesis: S₁[ succ A]
let W be set ; :: thesis: ( W is Tarski & succ A in On W implies ( card (Rank (succ A)) in card W & Rank (succ A) in W ) )
assume A2: ( W is Tarski & succ A in On W ) ; :: thesis: ( card (Rank (succ A)) in card W & Rank (succ A) in W )
then A3: ( A in succ A & card W = On W & W is subset-closed ) by Th10, ORDINAL1:10;
then A in On W by A2, ORDINAL1:19;
then Rank A in W by A1, A2;
then ( bool (Rank A) in W & Rank (succ A) = bool (Rank A) ) by A2, CLASSES1:34, CLASSES1:def 2;
hence ( card (Rank (succ A)) in card W & Rank (succ A) in W ) by A3, Th1; :: thesis: verum