let D be non empty Subset of (TOP-REAL 2); :: thesis: ( D = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} implies D ` = {(0.REAL 2)} )
assume A1: D = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} ; :: thesis: D ` = {(0.REAL 2)}
A2: {(0.REAL 2)} c= D `

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0.REAL 2)} or x in D ` )
assume A3: x in {(0.REAL 2)} ; :: thesis: x in D `
then not x in D by A1, XBOOLE_0:def 5;
then x in the carrier of (TOP-REAL 2) \ D by A3, XBOOLE_0:def 5;
hence x in D ` by SUBSET_1:def 5; :: thesis: verum

end;

D ` c= {(0.REAL 2)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D ` or x in {(0.REAL 2)} )
assume x in D ` ; :: thesis: x in {(0.REAL 2)}
then x in the carrier of (TOP-REAL 2) \ D by SUBSET_1:def 5;
then ( x in the carrier of (TOP-REAL 2) & not x in D ) by XBOOLE_0:def 5;
hence x in {(0.REAL 2)} by A1, XBOOLE_0:def 5; :: thesis: verum

end;

hence D ` = {(0.REAL 2)} by A2, XBOOLE_0:def 10; :: thesis: verum