take Theorems (X,R) ; :: thesis: ( Theorems (X,R) is X -extending & Theorems (X,R) is R -closed )
thus ( Theorems (X,R) is X -extending & Theorems (X,R) is R -closed ) ; :: thesis: verum