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