take {} T ; :: thesis: {} T is interval
thus {} T is interval ; :: thesis: verum