take Stop S ; :: thesis: ( not Stop S is halt-free & not Stop S is empty )
thus ( not Stop S is halt-free & not Stop S is empty ) ; :: thesis: verum