theorem po2: :: FIELD_12:48

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) st p <= q & q <= p holds
p = q