take {} ; :: thesis: {} is S -null
thus {} is S -null ; :: thesis: verum