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 ) )

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

( 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 S2
; :: thesis: a in S1assume
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;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

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