[FOM] ontology

[Freek Wiedijk]

>Are the finite ordinals the same mathematical objects as the
>finite cardinals?

In the Mizar world they are!

 theorem x is finite Ordinal iff x is finite Cardinal
 proof
  hereby
   assume x is finite Ordinal;
   then x is finite & x in omega by CARD_4:7;
   hence x is finite Cardinal by CARD_1:65;
  end;
  thus thesis;
 end;

(I couldn't find this as an already proven theorem in the
MML, but it wouldn't surprise me if it was there somewhere
already.)

Freek