let X be set ; :: thesis: for A being Ordinal holds
( X in Rank A iff ex B being Ordinal st
( B in A & X in bool (Rank B) ) )

let A be Ordinal; :: thesis: ( X in Rank A iff ex B being Ordinal st
( B in A & X in bool (Rank B) ) )

thus ( X in Rank A implies ex B being Ordinal st
( B in A & X in bool (Rank B) ) ) :: thesis: ( ex B being Ordinal st
( B in A & X in bool (Rank B) ) implies X in Rank A )
proof
assume A1: X in Rank A ; :: thesis: ex B being Ordinal st
( B in A & X in bool (Rank B) )

per cases ( A is limit_ordinal or not A is limit_ordinal ) ;
suppose A is limit_ordinal ; :: thesis: ex B being Ordinal st
( B in A & X in bool (Rank B) )

then consider B being Ordinal such that
A3: ( B in A & X in Rank B ) by ;
take B ; :: thesis: ( B in A & X in bool (Rank B) )
B c= B \/ {B} by XBOOLE_1:7;
then B c= succ B by ORDINAL1:def 1;
then Rank B c= Rank (succ B) by CLASSES1:37;
then X in Rank (succ B) by A3;
hence ( B in A & X in bool (Rank B) ) by ; :: thesis: verum
end;
suppose not A is limit_ordinal ; :: thesis: ex B being Ordinal st
( B in A & X in bool (Rank B) )

then consider B being Ordinal such that
A4: A = succ B by ORDINAL1:29;
take B ; :: thesis: ( B in A & X in bool (Rank B) )
thus ( B in A & X in bool (Rank B) ) by ; :: thesis: verum
end;
end;
end;
thus ( ex B being Ordinal st
( B in A & X in bool (Rank B) ) implies X in Rank A ) by ; :: thesis: verum