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