take R0 S ; :: thesis: R0 S is Correct
thus R0 S is Correct ; :: thesis: verum