take R ; :: thesis: R is R -extending
thus R is R -extending by Th1; :: thesis: verum