let f be ExtReal; :: thesis: {f} "" = {(f ")}
let i be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not i in {f} "" or i in {(f ")} ) & ( not i in {(f ")} or i in {f} "" ) )

hereby :: thesis: ( not i in {(f ")} or i in {f} "" )

assume i in {f} "" ; :: thesis: i in {(f ")}
then consider w being Element of ExtREAL such that
A1: i = w " and
A2: w in {f} ;
w = f by A2, TARSKI:def 1;
hence i in {(f ")} by A1, TARSKI:def 1; :: thesis: verum

end;

assume i in {(f ")} ; :: thesis: i in {f} ""
then A3: i = f " by TARSKI:def 1;
( f in ExtREAL & f in {f} ) by TARSKI:def 1, XXREAL_0:def 1;
hence i in {f} "" by A3; :: thesis: verum