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 p, q, r being Element of Ext_Set (f,E) st p <= q & q <= r holds
p <= r
let E be FieldExtension of F; :: thesis: for L being F -monomorphic Field
for f being Monomorphism of F,L
for p, q, r being Element of Ext_Set (f,E) st p <= q & q <= r holds
p <= r
let L be F -monomorphic Field; :: thesis: for f being Monomorphism of F,L
for p, q, r being Element of Ext_Set (f,E) st p <= q & q <= r holds
p <= r
let f be Monomorphism of F,L; :: thesis: for p, q, r being Element of Ext_Set (f,E) st p <= q & q <= r holds
p <= r
let p, q, r be Element of Ext_Set (f,E); :: thesis: ( p <= q & q <= r implies p <= r )
assume AS: ( p <= q & q <= r ) ; :: thesis: p <= r
then consider K1 being FieldExtension of p `1 , g1 being Function of K1,L such that
B: ( K1 = q `1 & g1 = q `2 & g1 is p `2 -extending ) ;
consider K2 being FieldExtension of q `1 , g2 being Function of K2,L such that
D: ( K2 = r `1 & g2 = r `2 & g2 is q `2 -extending ) by AS;
reconsider K = p `1 as Field ;
reconsider K1 = K1 as FieldExtension of K ;
reconsider K2 = K2 as K1 -extending FieldExtension of K by B;
reconsider L1 = L as FieldExtension of L by FIELD_4:6;
reconsider g = p `2 as Function of K,L ;
reconsider g2 = g2 as Function of K2,L1 ;

now :: thesis: for K being FieldExtension of p `1
for h being Function of K,L st K = r `1 & h = r `2 holds
h is p `2 -extending

let K be FieldExtension of p `1 ; :: thesis: for h being Function of K,L st K = r `1 & h = r `2 holds
h is p `2 -extending
let h be Function of K,L; :: thesis: ( K = r `1 & h = r `2 implies h is p `2 -extending )
assume F: ( K = r `1 & h = r `2 ) ; :: thesis: h is p `2 -extending
g2 is g -extending by B, D, FIELD_8:41;
hence h is p `2 -extending by F, D; :: thesis: verum

end;

hence p <= r by AS; :: thesis: verum