theorem Lm1: :: RING_3:43

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