theorem :: ORDINAL5:51

for a being Ordinal st a is epsilon holds
ex b being Ordinal st a = epsilon_ b