take J = I --> the non empty TopSpace; :: thesis: ( J is TopSpace-yielding & J is non-Empty )
thus ( J is TopSpace-yielding & J is non-Empty ) ; :: thesis: verum