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