let S1, S2 be ext-real-membered set ; :: thesis:
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:
for a being object holds
( a in S1 iff a in S2 )

proof

let a be object ; :: thesis:

hereby :: thesis:

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

end;

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

end;

hence S1 = S2 ; :: thesis: