:: deftheorem defines includes_an_isomorphic_copy_of RING_3:def 1 :
for R, S being Ring holds
( R includes_an_isomorphic_copy_of S iff ex T being strict Subring of R st T,S are_isomorphic );