take {} ; :: thesis: {} is trivial
thus {} is trivial ; :: thesis: verum