theorem po1: :: FIELD_12:47

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 being Element of Ext_Set (f,E) holds p <= p