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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. (TOP-REAL 2))} or x in D ` )
assume A3: x in {(0. (TOP-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. (TOP-REAL 2))}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D ` or x in {(0. (TOP-REAL 2))} )
assume x in D ` ; :: thesis: x in {(0. (TOP-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. (TOP-REAL 2))} by A1, XBOOLE_0:def 5; :: thesis: verum

end;

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