let F be Field; :: thesis: for E being FieldExtension of F
for L being F -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds p <= upper_bound S
let E be FieldExtension of F; :: thesis: for L being F -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds p <= upper_bound S
let L be F -monomorphic Field; :: thesis: for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds p <= upper_bound S
let f be Monomorphism of F,L; :: thesis: for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds p <= upper_bound S
let S be non empty ascending Subset of (Ext_Set (f,E)); :: thesis: for p being Element of S holds p <= upper_bound S
let p be Element of S; :: thesis: p <= upper_bound S
set q = upper_bound S;
set K = unionField (S,f,E);
set h = unionExt (S,f,E);
C: p `1 is Subfield of unionField (S,f,E) by Fsubb;

now :: thesis: for K1 being FieldExtension of p `1
for g1 being Function of K1,L st K1 = (upper_bound S) `1 & g1 = (upper_bound S) `2 holds
g1 is p `2 -extending

let K1 be FieldExtension of p `1 ; :: thesis: for g1 being Function of K1,L st K1 = (upper_bound S) `1 & g1 = (upper_bound S) `2 holds
g1 is p `2 -extending
let g1 be Function of K1,L; :: thesis: ( K1 = (upper_bound S) `1 & g1 = (upper_bound S) `2 implies g1 is p `2 -extending )
assume ( K1 = (upper_bound S) `1 & g1 = (upper_bound S) `2 ) ; :: thesis: g1 is p `2 -extending
then g1 | the carrier of (p `1) = p `2 by dufe;
hence g1 is p `2 -extending by FUNCT_1:49; :: thesis: verum

end;

hence p <= upper_bound S by C, FIELD_4:7; :: thesis: verum