take Sierpinski_Space ; :: thesis: ( Sierpinski_Space is injective & Sierpinski_Space is strict )
thus ( Sierpinski_Space is injective & Sierpinski_Space is strict ) ; :: thesis: verum