let Z be open Subset of REAL; :: thesis: ( 0 in Z implies (id Z) " {0} = {0} )
assume A1: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in (id Z) " {0} or x in {0} )
assume A2: x in (id Z) " {0} ; :: thesis: x in {0}
then x in dom (id Z) by FUNCT_1:def 7;
then A3: x in Z ;
(id Z) . x in {0} by A2, FUNCT_1:def 7;
hence x in {0} by A3, FUNCT_1:18; :: thesis: verum

end;

let x be object ; :: 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 A4: x = 0 by TARSKI:def 1;
then (id Z) . x = 0 by A1, FUNCT_1:18;
then A5: (id Z) . x in {0} by TARSKI:def 1;
x in dom (id Z) by A1, A4;
hence x in (id Z) " {0} by A5, FUNCT_1:def 7; :: thesis: verum