consider n being Element of omega ;
take n ; :: thesis: n is natural
thus n in omega ; :: according to ORDINAL1:def 13 :: thesis: verum