let Z be Subset of REAL; :: thesis: ( 0 in Z implies (id Z) " {0} = {0} )
assume 0 in Z ; :: thesis: (id Z) " {0} = {0}
then {0} c= Z by ZFMISC_1:31;
hence (id Z) " {0} = {0} by FUNCT_2:94; :: thesis: verum