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