let Y be non empty set ; :: thesis: %I Y = { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) }
set B0 = { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) } ;
A1: %I Y c= { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in %I Y or a in { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) } )
assume a in %I Y ; :: thesis: a in { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) }
then a in { {x} where x is Element of Y : verum } by EQREL_1:37;
then consider x being Element of Y such that
A2: a = {x} ;
reconsider y = x as Element of Y ;
reconsider B = {y} as Subset of Y by ZFMISC_1:31;
a = B by A2;
hence a in { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) } ; :: thesis: verum

end;

{ B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) } c= %I Y

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) } or x1 in %I Y )
assume x1 in { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) } ; :: thesis: x1 in %I Y
then ex B being Subset of Y st
( x1 = B & ex x being set st
( B = {x} & x in Y ) ) ;
then x1 in { {z} where z is Element of Y : verum } ;
hence x1 in %I Y by EQREL_1:37; :: thesis: verum

end;

hence %I Y = { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) } by A1, XBOOLE_0:def 10; :: thesis: verum