:: deftheorem defsubfr defines Subfield FIELD_6:def 2 :
for R being field-containing Ring
for b₂ being Field holds
( b₂ is Subfield of R iff b₂ is Subring of R );