take {(R#0 S)} ; :: thesis: not {(R#0 S)} is empty
thus not {(R#0 S)} is empty ; :: thesis: verum