take {(R0 S)} ; :: thesis: not {(R0 S)} is empty
thus not {(R0 S)} is empty ; :: thesis: verum