take IT = {} X; :: thesis: IT is finite
thus IT is finite ; :: thesis: verum