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 )
consider Y being set such that
A2: Y in X and
A3: A c= the_rank_of Y by A1, Th70, ORDINAL1:6;
take Y ; :: thesis: ( Y in X & the_rank_of Y = A )
the_rank_of Y c= A by A1, ORDINAL1:22, A2, Th68;
hence ( Y in X & the_rank_of Y = A ) by A2, A3; :: thesis: verum