:: 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;