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: D ` c= {(0. (TOP-REAL 2))}

proof

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

end;

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

proof

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

end;

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