let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume A1: S₁[A] ; :: thesis: S₁[ succ A]
A2: A in succ A by ORDINAL1:6;
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 that
A3: W is Tarski and
A4: succ A in On W ; :: thesis: ( card (Rank (succ A)) in card W & Rank (succ A) in W )
card W = On W by A3, Th9;
then A in On W by A4, A2, ORDINAL1:10;
then Rank A in W by A1, A3;
then A5: bool (Rank A) in W by A3;
Rank (succ A) = bool (Rank A) by CLASSES1:30;
hence ( card (Rank (succ A)) in card W & Rank (succ A) in W ) by A3, A5, Th1; :: thesis: verum