Prove:

(== => =) ,

under the assumption:

(Ex== => =) .

For proving (== => =) we take all variables arbitrary but fixed and prove:

(1) .

We prove (1) by the deduction rule.

We assume

(2)

and show

(3) .

The conjunction (2) splits into (4) , (5) .

For proving (3) , by (Ex== => =) , it suffices to prove

(7) .

For proving (7) it is sufficient to prove:

(8) .

We prove the individual conjunctive parts of (8) :

Proof of (9) :

Formula (9) is true because it is identical to (4) .

Proof of (10) :

Formula (10) is true because it is identical to (5) .

---

Converted by Mathematica      February 11, 2000