:: deftheorem defasc defines ascending FIELD_12:def 4 :
for f being Field-yielding sequence holds
( f is ascending iff for i being Element of NAT holds f . (i + 1) is FieldExtension of f . i );