set n = the Element of omega ;
take the Element of omega ; :: thesis: the Element of omega is finite
thus the Element of omega is finite ; :: thesis: verum