theorem po3: :: FIELD_12:49

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