:: deftheorem dA defines ClosureSequence FIELD_12:def 10 :
for F being Field
for b₂ being Field-yielding ascending sequence holds
( b₂ is ClosureSequence of F iff ( b₂ . 0 = F & ( for i being Element of NAT
for K being Field
for E being FieldExtension of K st K = b₂ . i & E = b₂ . (i + 1) holds
for p being non constant Element of the carrier of (Polynom-Ring K) holds p is_with_roots_in E ) ) );