take {} [:X,X:] ; :: thesis: {} [:X,X:] is empty
thus {} [:X,X:] is empty ; :: thesis: verum