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

( 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