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 being Element of Ext_Set (f,E) st p <= q & q <= p holds
p = q
let E be FieldExtension of F; :: thesis: for L being F -monomorphic Field
for f being Monomorphism of F,L
for p, q being Element of Ext_Set (f,E) st p <= q & q <= p holds
p = q
let L be F -monomorphic Field; :: thesis: for f being Monomorphism of F,L
for p, q being Element of Ext_Set (f,E) st p <= q & q <= p holds
p = q
let f be Monomorphism of F,L; :: thesis: for p, q being Element of Ext_Set (f,E) st p <= q & q <= p holds
p = q
let p, q be Element of Ext_Set (f,E); :: thesis: ( p <= q & q <= p implies p = q )
assume AS: ( p <= q & q <= p ) ; :: thesis: p = q
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 ) by AS;
E: ( p `1 is Subfield of q `1 & q `1 is Subfield of p `1 ) by AS, FIELD_4:7;
p `2 = q `2 by B, E, EC_PF_1:4;
hence p = q by E, EC_PF_1:4, XTUPLE_0:2; :: thesis: verum