take omega ; :: thesis: omega is limit_ordinal
thus omega is limit_ordinal by ORDINAL1:def 11; :: thesis: verum