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 )

proof

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

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

assume 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;

assume A5: a in S2 ; :: thesis: a in S1
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;

hence S1 = S2 ; :: thesis: verum