:: NUMERALS semantic presentation begin theorem :: NUMERALS:1 {} is Element of omega proof {} in omega by ORDINAL1:def_11; hence {} is Element of omega by SUBSET_1:def_1; ::_thesis: verum end;