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