take {} R ; :: thesis: {} R is finite
thus {} R is finite ; :: thesis: verum