for E, F being Field holds
( E includes F iff ex K being strict Subfield of E st K,F are_isomorphic )