theorem Th13: :: WAYBEL18:13

for I being non empty set holds { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum } is prebasis of (product (I --> Sierpinski_Space))