theorem Th15: :: FIELD_2:17

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F
for E being Field st E = embField f holds
K is Subfield of E