take Sierpinski_Space ; :: thesis: ( Sierpinski_Space is injective & Sierpinski_Space is monotone-convergence & not Sierpinski_Space is trivial )
thus ( Sierpinski_Space is injective & Sierpinski_Space is monotone-convergence & not Sierpinski_Space is trivial ) ; :: thesis: verum