let Z be open Subset of REAL ; :: thesis: ( 0 in Z implies (id Z) " {0 } = {0 } )
assume A: 0 in Z ; :: thesis: (id Z) " {0 } = {0 }
thus (id Z) " {0 } c= {0 } :: according to XBOOLE_0:def 10 :: thesis: {0 } c= (id Z) " {0 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (id Z) " {0 } or x in {0 } )
assume A3: x in (id Z) " {0 } ; :: thesis: x in {0 }
then x in dom (id Z) by FUNCT_1:def 13;
then A4: x in Z by FUNCT_1:34;
(id Z) . x in {0 } by A3, FUNCT_1:def 13;
hence x in {0 } by A4, FUNCT_1:35; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {0 } or x in (id Z) " {0 } )
assume x in {0 } ; :: thesis: x in (id Z) " {0 }
then Z0: x = 0 by TARSKI:def 1;
then (id Z) . x = 0 by A, FUNCT_1:35;
then Z1: (id Z) . x in {0 } by TARSKI:def 1;
x in dom (id Z) by A, Z0, FUNCT_1:34;
hence x in (id Z) " {0 } by Z1, FUNCT_1:def 13; :: thesis: verum