take omega --> 0 ; :: thesis: not omega --> 0 is finite
thus not omega --> 0 is finite ; :: thesis: verum