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