take R#0 S ; :: thesis: R#0 S is Correct
thus R#0 S is Correct ; :: thesis: verum