take Stop S ; :: thesis: not Stop S is empty
thus not Stop S is empty ; :: thesis: verum