:: deftheorem defines integral_closure ALGNUM_1:def 3 :
for A being non degenerated Ring
for B being Ring st A is Subring of B holds
integral_closure (A,B) = { z where z is Element of B : z is_integral_over A } ;