:: deftheorem defines upper_bound FIELD_12:def 24 :
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 ascending Subset of (Ext_Set (f,E)) holds upper_bound S = [(unionField (S,f,E)),(unionExt (S,f,E))];