:: deftheorem dasc defines ascending FIELD_12:def 16 :
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)) holds
( S is ascending iff for p, q being Element of S holds
( p <= q or q <= p ) );