theorem :: ORDINAL5:34

for a, b being Ordinal st a c= b holds
first_epsilon_greater_than a c= first_epsilon_greater_than b