theorem pr1: :: FIELD_5:12

for E being Field
for F being Subfield of E holds F is Subring of E