take Stop S ; :: thesis: ( Stop S is initial & not Stop S is empty )
thus ( Stop S is initial & not Stop S is empty ) ; :: thesis: verum