:: deftheorem defines is_embedded_in QUOFIELD:def 22 :
for R, S being non empty doubleLoopStr holds
( R is_embedded_in S iff ex f being Function of R,S st f is RingMonomorphism );