:: deftheorem defines <= FIELD_12:def 15 :
for F being Field
for E being FieldExtension of F
for L being b₁ -monomorphic Field
for f being Monomorphism of F,L
for p, q being Element of Ext_Set (f,E) holds
( p <= q iff ( q `1 is FieldExtension of p `1 & ( for K being FieldExtension of p `1
for g being Function of K,L st K = q `1 & g = q `2 holds
g is p `2 -extending ) ) );