for R being Ring
for S being Subring of R
for x being Element of S holds x is Element of R