{} in omega by ORDINAL1:def 12;
hence {} is Element of omega by SUBSET_1:def 2; :: thesis: verum