let A be Ordinal; :: thesis: On (Rank A) = A
thus On (Rank A) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= On (Rank A)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in On (Rank A) or x in A )
assume A1: x in On (Rank A) ; :: thesis: x in A
then reconsider B = x as Ordinal by ORDINAL1:def 9;
x in Rank A by A1, ORDINAL1:def 9;
then the_rank_of B in A by CLASSES1:66;
hence x in A by CLASSES1:73; :: thesis: verum
end;
On A c= On (Rank A) by CLASSES1:38, ORDINAL2:9;
hence A c= On (Rank A) by ORDINAL2:8; :: thesis: verum