theorem Th40: :: ORDINAL5:40

for e being epsilon Ordinal holds first_epsilon_greater_than e = e |^|^ omega