let S1, S2 be ext-real-membered set ; :: thesis: ( ( for a being ExtReal holds
( a in S1 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) ) & ( for a being ExtReal holds
( a in S2 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) ) implies S1 = S2 )
assume that
A2: for a being ExtReal holds
( a in S1 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) and
A3: for a being ExtReal holds
( a in S2 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) ; :: thesis: S1 = S2
let a be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not R14(a,S1) or not R14(a,S2) ) & ( not R14(a,S2) or not R14(a,S1) ) )

hereby :: thesis: ( not R14(a,S2) or not R14(a,S1) )

assume a in S1 ; :: thesis: a in S2
then ex A being non empty ext-real-membered set st
( A in F & a = sup A ) by A2;
hence a in S2 by A3; :: thesis: verum

end;

assume a in S2 ; :: thesis: R14(a,S1)
then ex A being non empty ext-real-membered set st
( A in F & a = sup A ) by A3;
hence R14(a,S1) by A2; :: thesis: verum