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