set M = { z where z is Element of B : z is_integral_over A } ;

A1: now :: thesis: for u being object st u in { z where z is Element of B : z is_integral_over A } holds
u in the carrier of B

let u be object ; :: thesis: ( u in { z where z is Element of B : z is_integral_over A } implies u in the carrier of B )
assume u in { z where z is Element of B : z is_integral_over A } ; :: thesis: u in the carrier of B
then ex z being Element of B st
( u = z & z is_integral_over A ) ;
hence u in the carrier of B ; :: thesis: verum

end;

In ((0. A),B) is_integral_over A by A0, Th27;
then 0. B is_integral_over A by A0, Lm5;
then 0. B in { z where z is Element of B : z is_integral_over A } ;
hence { z where z is Element of B : z is_integral_over A } is non empty Subset of B by A1, TARSKI:def 3; :: thesis: verum