H1: R is Subring of S by FIELD_4:def 1;
reconsider aR = a as Element of R by FIELD_7:def 5;
- a = - aR by H1, FIELD_6:17;
hence - a is R -membered by FIELD_7:def 5; :: thesis: verum