set IT = Sierpinski_Space ;
thus not Sierpinski_Space is empty by Def9; :: thesis: Sierpinski_Space is TopSpace-like
{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: ( ( for b₁ being Element of bool (bool the carrier of Sierpinski_Space ) holds
( not b₁ c= the topology of Sierpinski_Space or union b₁ in the topology of Sierpinski_Space ) ) & ( for b₁, b₂ being Element of bool the carrier of Sierpinski_Space holds
( not b₁ in the topology of Sierpinski_Space or not b₂ in the topology of Sierpinski_Space or b₁ /\ b₂ in the topology of Sierpinski_Space ) ) )
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: for b₁, b₂ being Element of bool the carrier of Sierpinski_Space holds
( not b₁ in the topology of Sierpinski_Space or not b₂ in the topology of Sierpinski_Space or b₁ /\ b₂ in the topology of Sierpinski_Space )

proof

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

per cases ( a = {} or a = {{} } or a = {{1}} or a = {{0 ,1}} or a = {{} ,{1}} or a = {{1},{0 ,1}} or a = {{} ,{0 ,1}} or a = {{} ,{1},{0 ,1}} ) by A1, ZFMISC_1:142;

suppose a = {} ; :: thesis: union a in the topology of Sierpinski_Space

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

end;

suppose a = {{} } ; :: thesis: union a in the topology of Sierpinski_Space

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

end;

suppose a = {{1}} ; :: thesis: union a in the topology of Sierpinski_Space

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

end;

suppose a = {{0 ,1}} ; :: thesis: union a in the topology of Sierpinski_Space

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

end;

suppose a = {{} ,{1}} ; :: thesis: union a in the topology of Sierpinski_Space

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

end;

suppose a = {{1},{0 ,1}} ; :: thesis: union a in the topology of Sierpinski_Space

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

end;

suppose a = {{} ,{0 ,1}} ; :: thesis: union a in the topology of Sierpinski_Space

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

end;

suppose a = {{} ,{1},{0 ,1}} ; :: thesis: union a in the topology of Sierpinski_Space

then a = {{} } \/ {{1},{0 ,1}} by ENUMSET1:42;
then union a = (union {{} }) \/ (union {{1},{0 ,1}}) by ZFMISC_1:96
.= {} \/ (union {{1},{0 ,1}}) by ZFMISC_1:31
.= {1} \/ {0 ,1} by ZFMISC_1:93
.= {0 ,1} by ZFMISC_1:14 ;
then union a in {{} ,{1},{0 ,1}} by ENUMSET1:def 1;
hence union a in the topology of Sierpinski_Space by Def9; :: thesis: verum

end;

end;

end;

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

per cases ( ( a = {} & b = {} ) or ( a = {} & b = {1} ) or ( a = {} & b = {0 ,1} ) or ( a = {1} & b = {} ) or ( a = {1} & b = {1} ) or ( a = {1} & b = {0 ,1} ) or ( a = {0 ,1} & b = {} ) or ( a = {0 ,1} & b = {1} ) or ( a = {0 ,1} & b = {0 ,1} ) ) by A2, ENUMSET1:def 1;

suppose ( a = {} & b = {} ) ; :: thesis: a /\ b in the topology of Sierpinski_Space

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

end;

suppose ( a = {} & b = {1} ) ; :: thesis: a /\ b in the topology of Sierpinski_Space

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

end;

suppose ( a = {} & b = {0 ,1} ) ; :: thesis: a /\ b in the topology of Sierpinski_Space

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

end;

suppose ( a = {1} & b = {} ) ; :: thesis: a /\ b in the topology of Sierpinski_Space

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

end;

suppose ( a = {1} & b = {1} ) ; :: thesis: a /\ b in the topology of Sierpinski_Space

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

end;

suppose ( a = {1} & b = {0 ,1} ) ; :: thesis: a /\ b in the topology of Sierpinski_Space

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

end;

suppose ( a = {0 ,1} & b = {} ) ; :: thesis: a /\ b in the topology of Sierpinski_Space

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

end;

suppose ( a = {0 ,1} & b = {1} ) ; :: thesis: a /\ b in the topology of Sierpinski_Space

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

end;

suppose ( a = {0 ,1} & b = {0 ,1} ) ; :: thesis: a /\ b in the topology of Sierpinski_Space

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

end;

end;