let X be set ; :: thesis: ( X is epsilon-transitive implies card (the_rank_of X) c= card X )
consider f being Function such that
A1: ( dom f = X & ( for x being object st x in X holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
assume A2: X is epsilon-transitive ; :: thesis: card (the_rank_of X) c= card X
the_rank_of X c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_rank_of X or x in rng f )
assume A3: x in the_rank_of X ; :: thesis: x in rng f
then reconsider x9 = x as Ordinal ;
consider Y being set such that
A4: Y in X and
A5: the_rank_of Y = x9 by A2, A3, Th40;
f . Y = x by A1, A4, A5;
hence x in rng f by A1, A4, FUNCT_1:def 3; :: thesis: verum

end;

hence card (the_rank_of X) c= card X by A1, CARD_1:12; :: thesis: verum