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 set ; :: 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 A2: a in %I Y ; :: thesis: a in { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) }
A3: a in { {x} where x is Element of Y : verum } by A2, EQREL_1:46;
consider x being Element of Y such that
A4: a = {x} by A3;
reconsider y = x as Element of Y ;
reconsider B = {y} as Subset of Y by ZFMISC_1:37;
A5: a = B by A4;
thus a in { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) } by A5; :: thesis: verum

end;

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

proof

let x1 be set ; :: 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 A7: x1 in { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) } ; :: thesis: x1 in %I Y
A8: ex B being Subset of Y st
( x1 = B & ex x being set st
( B = {x} & x in Y ) ) by A7;
A9: x1 in { {z} where z is Element of Y : verum } by A8;
thus x1 in %I Y by A9, EQREL_1:46; :: thesis: verum

end;

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