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))}

assume A1: D = NonZero (TOP-REAL 2) ; :: thesis: D ` = {(0. (TOP-REAL 2))}

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

proof

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

proof

hence
D ` = {(0. (TOP-REAL 2))}
by A2; :: thesis: verum
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;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