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