:: deftheorem deffc defines field-containing FIELD_6:def 1 :
for R being Ring holds
( R is field-containing iff ex F being Field st F is Subring of R );