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

proof

let x be set ; :: 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 x' = x as Ordinal ;
consider Y being set such that
A4: ( Y in X & the_rank_of Y = x' ) by A1, A3, Th41;
f . Y = x by A2, A4;
hence x in rng f by A2, A4, FUNCT_1:def 5; :: thesis: verum

end;

hence card (the_rank_of X) c= card X by A2, CARD_1:28; :: thesis: verum