:: deftheorem Def11 defines Ring_DOMAIN-like RINGCAT1:def 11 :
for IT being set holds
( IT is Ring_DOMAIN-like iff for x being Element of IT holds x is strict Ring );