take n = the Element of omega ; :: thesis: n is natural
thus n in omega ; :: according to ORDINAL1:def 12 :: thesis: verum