for K being Field
for F being b₁ -monomorphic Field st K,F are_disjoint holds
ex E being Field st
( E,F are_isomorphic & K is Subfield of E )