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 K19(K19( 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 K19( 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 K19( 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:118;

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:25;
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:25;
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:25;
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:75;
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: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: verum

end;

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

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

end;

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

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: 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:13;
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:13;
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;