let R be Ring; :: thesis: for S being Subring of R holds Char S = Char R
let S be Subring of R; :: thesis: Char S = Char R
R is S -monomorphic by Th70;
hence Char S = Char R by Th87; :: thesis: verum