When deciding whether it should be a construction in the language there are several parameters to take into account.
First of all whether it makes sense, which I clearly think the construction does: It is a "pure" logical operation that is faithful to the original declarative/logical reading of the Prolog languages.
Secondly whether it will actually be used, here I have a little more doubt: I guess that Martin that gave the suggestion will use it "extensively", perhaps because he programs more in logical terms than we actually do at PDC (I doubt that we will use it much, if at all, here).
Thirdly, whether alternative code (using already existing constructions) is complex and "unpleasant" or simple and "nice". The alternative code using two negations, comes from the normal logical duality of existential and universal quantifiers: If it is not possible to find "something" that does not fulfils "something", then every thing fulfills "something". Though this is a fundamental property of logic, the code with two nested nots, is both clumsy and unintuitive.
Fourthly it is also necessary to find good syntax for the construction. Good syntax should express the intuition of the semantics. Both so that people that read the code without knowing the construction in complete details, gets the correct idea about what it does, but also so that when they are looking for a construction that does something, they guess that this may be the one that does what they are looking for.
I think this construction qualifies on making sense and not having good alternative code, but I think it disqualifies on usability and syntax (also considering that there exist a mathematical paper that uses for all ... holds ...).