thus not 1. S is zero ; :: thesis: 1. S is R -membered
R is Subring of S by FIELD_4:def 1;
then 1. S = 1. R by C0SP1:def 3;
hence 1. S is R -membered by FIELD_7:def 5; :: thesis: verum