take omega ; :: thesis: not omega is finite
thus not omega is finite ; :: thesis: verum