theorem Th7: :: LIOUVIL2:6
for R being Ring
for S being Subring of R
for x being Element of S holds x is Element of R