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}

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

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 {0} or x in (id Z) " {0} )
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;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

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