theorem :: ORDINAL5:35

for a, b being Ordinal st a in b & b in first_epsilon_greater_than a holds
first_epsilon_greater_than b = first_epsilon_greater_than a