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 )
A2: A in succ A by ORDINAL1:10;
consider Y being set such that
A3: Y in X and
A4: A c= the_rank_of Y by A1, A2, Th78;
take Y ; :: thesis: ( Y in X & the_rank_of Y = A )
A5: the_rank_of Y in the_rank_of X by A3, Th76;
A6: the_rank_of Y c= A by A1, A5, ORDINAL1:34;
thus ( Y in X & the_rank_of Y = A ) by A3, A4, A6, XBOOLE_0:def 10; :: thesis: verum