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