:: deftheorem Def9 defines Sierpinski_Space WAYBEL18:def 9 :
for b₁ being strict TopStruct holds
( b₁ = Sierpinski_Space iff ( the carrier of b₁ = {0,1} & the topology of b₁ = {{},{1},{0,1}} ) );