set p = the Element of Ext_Set (f,E);
set S = { the Element of Ext_Set (f,E)};

now :: thesis: for o being object st o in { the Element of Ext_Set (f,E)} holds
o in Ext_Set (f,E)

let o be object ; :: thesis: ( o in { the Element of Ext_Set (f,E)} implies o in Ext_Set (f,E) )
assume o in { the Element of Ext_Set (f,E)} ; :: thesis: o in Ext_Set (f,E)
then o = the Element of Ext_Set (f,E) by TARSKI:def 1;
hence o in Ext_Set (f,E) ; :: thesis: verum

end;

then { the Element of Ext_Set (f,E)} c= Ext_Set (f,E) ;
then reconsider S = { the Element of Ext_Set (f,E)} as non empty Subset of (Ext_Set (f,E)) ;
take S ; :: thesis: S is ascending

now :: thesis: for q1, q2 being Element of S holds
( q1 <= q2 or q2 <= q1 )

let q1, q2 be Element of S; :: thesis: ( q1 <= q2 or q2 <= q1 )
B: ( q1 = the Element of Ext_Set (f,E) & q2 = the Element of Ext_Set (f,E) ) by TARSKI:def 1;
for K being FieldExtension of the Element of Ext_Set (f,E) `1
for g being Function of K,L st K = the Element of Ext_Set (f,E) `1 & g = the Element of Ext_Set (f,E) `2 holds
g is the Element of Ext_Set (f,E) `2 -extending ;
hence ( q1 <= q2 or q2 <= q1 ) by B, FIELD_4:6; :: thesis: verum

end;

hence S is ascending ; :: thesis: verum