theorem :: FIELD_5:13

for F being Field
for R being Subring of F holds
( R is Subfield of F iff R is Field )