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