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 A1, CLASSES1:29, CLASSES1:31;
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 A3, CLASSES1:30; :: 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 A1, A4, ORDINAL1:6, CLASSES1:30; :: 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 CLASSES1:36, CLASSES1:41; :: thesis: verum