let R be Ring; :: thesis: for S being Subring of R
for x being Element of S holds x is Element of R
let S be Subring of R; :: thesis: for x being Element of S holds x is Element of R
let x be Element of S; :: thesis: x is Element of R
the carrier of S c= the carrier of R by C0SP1:def 3;
hence x is Element of R ; :: thesis: verum