theorem Th96: :: MATGRP_0:83

for R being Ring
for n being Nat
for S being Subring of R holds
( One (S,n) = One (R,n) & Zero (S,n) = Zero (R,n) ) by Th95, Th94;