let X be set ; :: thesis: for A being Ordinal holds
( the_rank_of X c= A iff for Y being set st Y in X holds
the_rank_of Y in A )
let A be Ordinal; :: thesis: ( the_rank_of X c= A iff for Y being set st Y in X holds
the_rank_of Y in A )
set R = the_rank_of X;
A1: X c= Rank (the_rank_of X) by Def9;
thus ( the_rank_of X c= A implies for Y being set st Y in X holds
the_rank_of Y in A ) by A1, Th66; :: thesis: ( ( for Y being set st Y in X holds
the_rank_of Y in A ) implies the_rank_of X c= A )
assume A2: for Y being set st Y in X holds
the_rank_of Y in A ; :: thesis: the_rank_of X c= A
X c= Rank A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank A )
reconsider xx = x as set by TARSKI:1;
assume x in X ; :: thesis: x in Rank A
then the_rank_of xx in A by A2;
hence x in Rank A by Th66; :: thesis: verum
end;
hence the_rank_of X c= A by Def9; :: thesis: verum