R is Subring of S by FIELD_4:def 1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
hence a is Element of S ; :: thesis: verum