set IT = Sierpinski_Space ;
thus not Sierpinski_Space is empty by Def9; :: thesis:
{0,1} in {{},{1},{0,1}} by ENUMSET1:def 1;
then the carrier of Sierpinski_Space in {{},{1},{0,1}} by Def9;
hence the carrier of Sierpinski_Space in the topology of Sierpinski_Space by Def9; :: according to PRE_TOPC:def 1 :: thesis:
thus for a being Subset-Family of Sierpinski_Space st a c= the topology of Sierpinski_Space holds
union a in the topology of Sierpinski_Space :: thesis:

proof

let a be Subset-Family of Sierpinski_Space; :: thesis:
assume a c= the topology of Sierpinski_Space ; :: thesis:
then A1: a c= {{},{1},{0,1}} by Def9;

per cases by A1, ZFMISC_1:118;

suppose a = {} ; :: thesis:

then union a in {{},{1},{0,1}} by ENUMSET1:def 1, ZFMISC_1:2;
hence union a in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose a = {{}} ; :: thesis:

then union a = {} by ZFMISC_1:25;
then union a in {{},{1},{0,1}} by ENUMSET1:def 1;
hence union a in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose a = {{1}} ; :: thesis:

then union a = {1} by ZFMISC_1:25;
then union a in {{},{1},{0,1}} by ENUMSET1:def 1;
hence union a in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose a = {{0,1}} ; :: thesis:

then union a = {0,1} by ZFMISC_1:25;
then union a in {{},{1},{0,1}} by ENUMSET1:def 1;
hence union a in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose a = {{},{1}} ; :: thesis:

then union a = {} \/ {1} by ZFMISC_1:75;
then union a in {{},{1},{0,1}} by ENUMSET1:def 1;
hence union a in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose a = {{1},{0,1}} ; :: thesis:

then union a = {1} \/ {0,1} by ZFMISC_1:75
.= {0,1} by ZFMISC_1:9 ;
then union a in {{},{1},{0,1}} by ENUMSET1:def 1;
hence union a in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose a = {{},{0,1}} ; :: thesis:

then union a = {} \/ {0,1} by ZFMISC_1:75;
then union a in {{},{1},{0,1}} by ENUMSET1:def 1;
hence union a in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose a = {{},{1},{0,1}} ; :: thesis:

then a = {{}} \/ {{1},{0,1}} by ENUMSET1:2;
then union a = (union {{}}) \/ (union {{1},{0,1}}) by ZFMISC_1:78
.= {} \/ (union {{1},{0,1}}) by ZFMISC_1:25
.= {1} \/ {0,1} by ZFMISC_1:75
.= {0,1} by ZFMISC_1:9 ;
then union a in {{},{1},{0,1}} by ENUMSET1:def 1;
hence union a in the topology of Sierpinski_Space by Def9; :: thesis:

end;

end;

end;

let a, b be Subset of Sierpinski_Space; :: thesis:
assume ( a in the topology of Sierpinski_Space & b in the topology of Sierpinski_Space ) ; :: thesis:
then A2: ( a in {{},{1},{0,1}} & b in {{},{1},{0,1}} ) by Def9;

per cases by A2, ENUMSET1:def 1;

suppose ( a = {} & b = {} ) ; :: thesis:

then a /\ b in {{},{1},{0,1}} by ENUMSET1:def 1;
hence a /\ b in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose ( a = {} & b = {1} ) ; :: thesis:

then a /\ b in {{},{1},{0,1}} by ENUMSET1:def 1;
hence a /\ b in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose ( a = {} & b = {0,1} ) ; :: thesis:

then a /\ b in {{},{1},{0,1}} by ENUMSET1:def 1;
hence a /\ b in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose ( a = {1} & b = {} ) ; :: thesis:

then a /\ b in {{},{1},{0,1}} by ENUMSET1:def 1;
hence a /\ b in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose ( a = {1} & b = {1} ) ; :: thesis:

then a /\ b in {{},{1},{0,1}} by ENUMSET1:def 1;
hence a /\ b in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose ( a = {1} & b = {0,1} ) ; :: thesis:

then a /\ b = {1} by ZFMISC_1:13;
then a /\ b in {{},{1},{0,1}} by ENUMSET1:def 1;
hence a /\ b in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose ( a = {0,1} & b = {} ) ; :: thesis:

then a /\ b in {{},{1},{0,1}} by ENUMSET1:def 1;
hence a /\ b in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose ( a = {0,1} & b = {1} ) ; :: thesis:

then a /\ b = {1} by ZFMISC_1:13;
then a /\ b in {{},{1},{0,1}} by ENUMSET1:def 1;
hence a /\ b in the topology of Sierpinski_Space by Def9; :: thesis:

end;

suppose ( a = {0,1} & b = {0,1} ) ; :: thesis:

then a /\ b in {{},{1},{0,1}} by ENUMSET1:def 1;
hence a /\ b in the topology of Sierpinski_Space by Def9; :: thesis:

end;

end;