Let m be given.

Assume Hm.

Apply ordinal_Subq_SNoLe 0 m ordinal_Empty (nat_p_ordinal m (omega_nat_p m Hm)) to the current goal.

We will prove 0 ⊆ m.

Apply Subq_Empty to the current goal.

∎