take {} T ; :: thesis: ( {} T is empty & {} T is compact )
thus ( {} T is empty & {} T is compact ) ; :: thesis: verum