for R being Ring
for S being Subring of R
for r being Element of R
for s being Element of S st r = s & s is_integral_over S holds
r is_integral_over R