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