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 = inf A ) ) ) & ( for a being ExtReal holds

( a in S2 iff ex A being non empty ext-real-membered set st

( A in F & a = inf 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 = inf 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 = inf A ) ) ; :: thesis: S1 = S2

for a being object holds

( a in S1 iff a in S2 )

( a in S1 iff ex A being non empty ext-real-membered set st

( A in F & a = inf A ) ) ) & ( for a being ExtReal holds

( a in S2 iff ex A being non empty ext-real-membered set st

( A in F & a = inf 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 = inf 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 = inf A ) ) ; :: thesis: S1 = S2

for a being object holds

( a in S1 iff a in S2 )

proof

hence
S1 = S2
; :: thesis: verum
let a be object ; :: thesis: ( a in S1 iff a in S2 )

then reconsider a = a as ExtReal ;

ex A being non empty ext-real-membered set st

( A in F & a = inf A ) by A3, A5;

hence a in S1 by A2; :: thesis: verum

end;hereby :: thesis: ( a in S2 implies a in S1 )

assume A5:
a in S2
; :: thesis: a in S1assume A4:
a in S1
; :: thesis: a in S2

then reconsider a9 = a as ExtReal ;

ex A being non empty ext-real-membered set st

( A in F & a9 = inf A ) by A2, A4;

hence a in S2 by A3; :: thesis: verum

end;then reconsider a9 = a as ExtReal ;

ex A being non empty ext-real-membered set st

( A in F & a9 = inf A ) by A2, A4;

hence a in S2 by A3; :: thesis: verum

then reconsider a = a as ExtReal ;

ex A being non empty ext-real-membered set st

( A in F & a = inf A ) by A3, A5;

hence a in S1 by A2; :: thesis: verum