theorem lem1a: :: FIELD_12:50

for F being Field
for E being FieldExtension of F
for L being b₁ -monomorphic Field
for f being Monomorphism of F,L
for S being non empty Subset of (Ext_Set (f,E))
for p, q being Element of S
for a being Element of (p `1) st p <= q holds
a in the carrier of (q `1)