let X be set ; :: thesis: for A being Ordinal st the_rank_of X = succ A holds
ex Y being set st
( Y in X & the_rank_of Y = A )
let A be Ordinal; :: thesis: ( the_rank_of X = succ A implies ex Y being set st
( Y in X & the_rank_of Y = A ) )
assume A1: the_rank_of X = succ A ; :: thesis: ex Y being set st
( Y in X & the_rank_of Y = A )
then ( A in succ A & succ A c= the_rank_of X ) by ORDINAL1:10;
then consider Y being set such that
A2: ( Y in X & A c= the_rank_of Y ) by Th78;
take Y ; :: thesis: ( Y in X & the_rank_of Y = A )
the_rank_of Y in the_rank_of X by A2, Th76;
then the_rank_of Y c= A by A1, ORDINAL1:34;
hence ( Y in X & the_rank_of Y = A ) by A2, XBOOLE_0:def 10; :: thesis: verum