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 ; :: thesis: verum