set IT = Sierpinski_Space ;
thus
not Sierpinski_Space is empty
by Def9; 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; PRE_TOPC:def 1 ( ( for b1 being Element of K19(K19( the carrier of Sierpinski_Space)) holds
( not b1 c= the topology of Sierpinski_Space or union b1 in the topology of Sierpinski_Space ) ) & ( for b1, b2 being Element of K19( the carrier of Sierpinski_Space) holds
( not b1 in the topology of Sierpinski_Space or not b2 in the topology of Sierpinski_Space or b1 /\ b2 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
for b1, b2 being Element of K19( the carrier of Sierpinski_Space) holds
( not b1 in the topology of Sierpinski_Space or not b2 in the topology of Sierpinski_Space or b1 /\ b2 in the topology of Sierpinski_Space )proof
let a be
Subset-Family of
Sierpinski_Space;
( a c= the topology of Sierpinski_Space implies union a in the topology of Sierpinski_Space )
assume
a c= the
topology of
Sierpinski_Space
;
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 = {{},{1},{0,1}}
;
union a in the topology of Sierpinski_Spacethen
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;
verum end; end;
end;
let a, b be Subset of Sierpinski_Space; ( 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 )
; a /\ b in the topology of Sierpinski_Space
then A2:
( a in {{},{1},{0,1}} & b in {{},{1},{0,1}} )
by Def9;