take {} ; :: thesis: {} is R-normal
thus {} is R-normal ; :: thesis: verum