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 a in S1 or a in S2 ) & ( not a in S2 or a in S1 ) )
hereby :: thesis: ( not a in S2 or a in 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: a in S1
then ex A being non empty ext-real-membered set st
( A in F & a = sup A ) by A3;
hence a in S1 by A2; :: thesis: verum