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