The classification of the agreement conditions provided above is complete, in the sense that there is no other possible configuration of EGG/YOLKs, as shown by Lehmann and Cohn in (1994). Based on the completeness of that analysis, we can show the following results.

## Theorem 1 Mnd For Bilateral Mn Is Consistent.

Proof Consider two agents represented in the MND system with sets LS1 and LS2 of stubbornness formulas and sets LF1 and LF2 of flexible formulas. To prove that MND
is consistent, we show that if a Σiformula ξ is inferred using the MND rules, or, in other terms, is deduced as a theorem in the system, then ξ represents a proposal that is acceptable by both agents. In other words, we aim at proving that when the rules yield ξ then ξ generalizes both LF1 and LF2 and is generalized by both LS1 and LS2
.

To prove this, we need to show that:
(i) The rules for making new proposals yield a relation that is acceptable from the viewpoint of the agent who made the proposal before and infer a new proposal again still acceptable. In other terms, if an agent makes a proposal that is generalized by the set of stubbornness formulas LSi
, and is a generalization of the set of flexible formulas LFi
, for one agent, the rules infer a new proposal that is in the same relationships with LSi and LFi
.

(ii) The rules for the second proposing agent infer the relation between the agents at that step of the negotiation.

(iii) The rules for the following proposing agent do the same as the rules for the second proposing agent, taking into account that this step takes place after the step of the second proposing agent.

(iv) The system transition rules close the negotiation only when the proposal is acceptable by both agents, namely generalizes both LFi and is generalized by both LSi sets.

Let us now consider a formula ξ that is acceptable by the two agents, and let us consider the rules that produce transitions in the system. In particular, if ξ is inferred by means of one of the rules (AD), (ED), (I), (Co), (Ag) for the second proposing agent, or by means of one of the rules given in Fig. 3 for the following proposing agent, then the possible results of the step described above are given by the application of the system transition rules. Evidently, if ξ is inferred, then the rule (D) does not apply. If (N) applies, and one more inference is performed, then the rules (W), (C), (S) allow us to infer a different formula. Suppose now, by contradiction, that the new formula ξ is not acceptable by one of the agents (in the sense that either is not a generalization of her set of flexible formulas or it is not generalized by the set of stubbornness formulas. As a consequence, one agent has called herself away, as we stated above. This, however, is impossible, by construction of the rules for the second and following proposals. Conversely, if the transition rule (D) applies and, therefore, the agents have incompatible viewpoints, then ξ is not inferred through the system, because it is not a generalization of both flexible sets of formulas and generalizes by both stubbornness sets of formulas. Clearly, by means of the full set of rules, it is not possible to do so when the agents have consistent viewpoints. 

We say that a deductive system is adequate to represent a MN between two agents when it infers an outcome iff an agreement is reachable between the agents, otherwise it does not produce any result.