take Stop S ; :: thesis: Stop S is closed
thus Stop S is closed ; :: thesis: verum