A1: 1 in {0,1} by TARSKI:def 2;
( the carrier of Sierpinski_Space = {0,1} & 0 in {0,1} ) by TARSKI:def 2, WAYBEL18:def 9;
hence ( not Sierpinski_Space is trivial & Sierpinski_Space is monotone-convergence ) by A1; :: thesis: verum