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 ) }

( B = {x} & x in Y ) } c= %I Y

( B = {x} & x in Y ) } by A1, XBOOLE_0:def 10; :: thesis: verum

( 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

{ B where B is Subset of Y : ex x being set st
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 = {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

( B = {x} & x in Y ) } c= %I Y

proof

hence
%I Y = { B where B is Subset of Y : ex x being set st
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;( 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

( B = {x} & x in Y ) } by A1, XBOOLE_0:def 10; :: thesis: verum