set M = { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } ;

now :: thesis: for U being Subring of S st R is Subring of U & T is Subset of U holds
1. S in U

let U be Subring of S; :: thesis: ( R is Subring of U & T is Subset of U implies 1. S in U )
assume ( R is Subring of U & T is Subset of U ) ; :: thesis: 1. S in U
1. U = 1. S by C0SP1:def 3;
hence 1. S in U ; :: thesis: verum

end;

then A: 1. S in { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } ;

now :: thesis: for o being object st o in { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } holds
o in the carrier of S

let o be object ; :: thesis: ( o in { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } implies o in the carrier of S )
assume o in { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } ; :: thesis: o in the carrier of S
then consider x being Element of S such that
H: ( o = x & ( for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U ) ) ;
thus o in the carrier of S by H; :: thesis: verum

end;

hence { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } is non empty Subset of S by TARSKI:def 3, A; :: thesis: verum