theorem Th36: :: ORDINAL5:36

first_epsilon_greater_than 0 = omega |^|^ omega