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