Description: An ordinal number has the ordinal property. (Contributed by NM, 5Jun1994)
Ref  Expression  

Assertion  eloni   ( A e. On > Ord A ) 
Step  Hyp  Ref  Expression 

1  elong   ( A e. On > ( A e. On <> Ord A ) ) 

2  1  ibi   ( A e. On > Ord A ) 