take omega --> 0 ; :: thesis: omega --> 0 is infinite
thus omega --> 0 is infinite ; :: thesis: verum