theorem Th85: :: MATGRP_0:72

for R being Ring
for n being Nat
for S being Subring of R holds n -Matrices_over S c= n -Matrices_over R