let q1, q2 be Element of unionCarrier (S,f,E); :: thesis: ( ex p being Element of S st q1 = 1. (p `1) & ex p being Element of S st q2 = 1. (p `1) implies q1 = q2 )
assume A1: ( ex p1 being Element of S st q1 = 1. (p1 `1) & ex p2 being Element of S st q2 = 1. (p2 `1) ) ; :: thesis: q1 = q2
then consider p1 being Element of S such that
A2: q1 = 1. (p1 `1) ;
consider p2 being Element of S such that
A3: q2 = 1. (p2 `1) by A1;

per cases ( p1 <= p2 or p2 <= p1 ) by dasc;

suppose p1 <= p2 ; :: thesis: q1 = q2

then p1 `1 is Subfield of p2 `1 by FIELD_4:7;
hence q1 = q2 by A2, A3, EC_PF_1:def 1; :: thesis: verum

end;

suppose p2 <= p1 ; :: thesis: q1 = q2

then p2 `1 is Subfield of p1 `1 by FIELD_4:7;
hence q1 = q2 by A2, A3, EC_PF_1:def 1; :: thesis: verum

end;

end;