numerals.miz

    begin

    theorem :: NUMERALS:1

     {} is Element of omega

    proof

       {} in omega by ORDINAL1:def 11;

      hence thesis by SUBSET_1:def 1;

    end;